Index: /trunk/Comorphisms/CASL2CspCASL.hs
===================================================================
--- /trunk/Comorphisms/CASL2CspCASL.hs (revision 11215)
+++ /trunk/Comorphisms/CASL2CspCASL.hs (revision 11216)
@@ -44,5 +44,5 @@
                CspCASLSign
                CspMorphism
-               () () () where
+               Symbol RawSymbol () where
     sourceLogic CASL2CspCASL = CASL
     sourceSublogic CASL2CspCASL = SL.top
Index: /trunk/Comorphisms/CspCASL2Modal.hs
===================================================================
--- /trunk/Comorphisms/CspCASL2Modal.hs (revision 11215)
+++ /trunk/Comorphisms/CspCASL2Modal.hs (revision 11216)
@@ -45,5 +45,5 @@
                CspCASLSign
                CspMorphism
-               () () ()
+               Symbol RawSymbol ()
                Modal ()
                M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
@@ -77,5 +77,5 @@
 
 
-mapSym :: () -> Symbol
+mapSym :: Symbol -> Symbol
 mapSym = error "CspCASL2Modal.mapSym not yet implemented"
    -- needs to be changed once modal symbols are added
Index: /trunk/Comorphisms/CspCASL2IsabelleHOL.hs
===================================================================
--- /trunk/Comorphisms/CspCASL2IsabelleHOL.hs (revision 11215)
+++ /trunk/Comorphisms/CspCASL2IsabelleHOL.hs (revision 11216)
@@ -18,4 +18,6 @@
 
 import CASL.AS_Basic_CASL
+import CASL.Sign (Symbol)
+import CASL.Morphism (RawSymbol)
 import qualified CASL.Inject as CASLInject
 import qualified CASL.Sign as CASLSign
@@ -53,5 +55,5 @@
                CspCASLSign
                CspMorphism
-               () () ()
+               Symbol RawSymbol ()
                Isabelle () () IsaSign.Sentence () ()
                IsaSign.Sign
Index: /trunk/CspCASL/StatAnaCSP.hs
===================================================================
--- /trunk/CspCASL/StatAnaCSP.hs (revision 11215)
+++ /trunk/CspCASL/StatAnaCSP.hs (revision 11216)
@@ -30,4 +30,5 @@
 import CASL.Overload (minExpFORMULA, oneExpTerm)
 import CASL.Sign
+import CASL.Morphism (RawSymbol)
 import CASL.StaticAna (allOpIds, allPredIds)
 import Common.AS_Annotation
@@ -49,5 +50,5 @@
 
 basicAnalysisCspCASL :: (CspBasicSpec, CspCASLSign, GlobalAnnos)
-        -> Result (CspBasicSpec, ExtSign CspCASLSign (),
+        -> Result (CspBasicSpec, ExtSign CspCASLSign Symbol,
                    [Named CspCASLSen])
 basicAnalysisCspCASL (cc, sigma, ga) =
Index: /trunk/CspCASL/Logic_CspCASL.hs
===================================================================
--- /trunk/CspCASL/Logic_CspCASL.hs (revision 11215)
+++ /trunk/CspCASL/Logic_CspCASL.hs (revision 11216)
@@ -75,5 +75,5 @@
     SignCSP.CspCASLSign     -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (?)
+    Symbol               -- symbol
     where
       parse_sentence CspCASL = Nothing
@@ -107,6 +107,6 @@
     SignCSP.CspCASLSign         -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (missing)
-    ()                      -- raw_symbol (missing)
+    Symbol
+    RawSymbol
     ()                      -- proof_tree (missing)
     where
@@ -123,6 +123,6 @@
     SignCSP.CspCASLSign         -- signature
     SignCSP.CspMorphism     -- morphism
-    ()                      -- symbol (missing)
-    ()                      -- raw_symbol (missing)
+    Symbol
+    RawSymbol
     where
       basic_analysis CspCASL =
Index: /trunk/CASL/AS_Basic_CASL.der.hs
===================================================================
--- /trunk/CASL/AS_Basic_CASL.der.hs (revision 11201)
+++ /trunk/CASL/AS_Basic_CASL.der.hs (revision 11216)
@@ -323,5 +323,5 @@
 
 data SYMB_KIND = Implicit | Sorts_kind
-               | Ops_kind | Preds_kind
+               | Ops_kind | Preds_kind | OtherKinds String
                  deriving (Show, Eq, Ord)
 
Index: /trunk/CASL/Sign.hs
===================================================================
--- /trunk/CASL/Sign.hs (revision 11204)
+++ /trunk/CASL/Sign.hs (revision 11216)
@@ -40,24 +40,10 @@
 
 data SymbType = SortAsItemType
+              | OtherTypeKind String
               | OpAsItemType OpType
                 -- since symbols do not speak about totality, the totality
                 -- information in OpType has to be ignored
               | PredAsItemType PredType
-                deriving Show
-
--- Ordering and equality of symbol types has to ingore totality information
-instance Ord SymbType where
-  compare st1 st2 = case (st1, st2) of
-    (SortAsItemType, SortAsItemType) -> EQ
-    (SortAsItemType, _) -> LT
-    (OpAsItemType ot1, OpAsItemType ot2) ->
-      compare (opArgs ot1, opRes ot1) (opArgs ot2, opRes ot2)
-    (OpAsItemType _, SortAsItemType) -> GT
-    (OpAsItemType _, PredAsItemType _) -> LT
-    (PredAsItemType pt1, PredAsItemType pt2) -> compare pt1 pt2
-    (PredAsItemType _, _) -> GT
-
-instance Eq SymbType where
-  t1 == t2 = compare t1 t2 == EQ
+                deriving (Show, Eq, Ord)
 
 data Symbol = Symbol {symName :: Id, symbType :: SymbType}