diff --git a/src/TPDB/Data.hs b/src/TPDB/Data.hs
--- a/src/TPDB/Data.hs
+++ b/src/TPDB/Data.hs
@@ -1,3 +1,8 @@
+-- | Data types for rewrite systems and termination problems.
+-- A "bare" term rewrite system (list of rules and relative rules) is @TRS v s@.
+-- A termination problem is @Problem v s@. This contains a rewrite system plus extra
+-- information (strategy, theory, etc.)
+
 {-# language DeriveDataTypeable #-}
 
 module TPDB.Data 
@@ -20,10 +25,10 @@
 import Data.Hashable
 import Data.Function (on)
 
-data Identifier = 
+data Identifier =
      Identifier { _identifier_hash :: ! Int
-                , name :: ! String 
-                , arity :: Int 
+                , name :: ! String
+                , arity :: Int
                 }
     deriving ( Eq, Ord, Typeable )
 
@@ -39,8 +44,26 @@
 
 ---------------------------------------------------------------------
 
+-- | according to XTC spec
+data Funcsym = Funcsym
+  { fs_name :: String -- ^ should be Text
+  , fs_arity :: Int
+  , fs_theory :: Maybe Theory
+  , fs_replacementmap :: Maybe Replacementmap
+  }
+  deriving (Show, Typeable)
 
-data RS s r = 
+data Signature = Signature [ Funcsym ]
+               | HigherOrderSignature
+  deriving (Show, Typeable)
+
+data Replacementmap = Replacementmap [Int]
+  deriving (Show, Typeable)
+
+---------------------------------------------------------------------
+
+
+data RS s r =
      RS { signature :: [ s ] -- ^ better keep order in signature (?)
         , rules :: [ Rule r ]
         , separate :: Bool -- ^ if True, write comma between rules
@@ -53,36 +76,47 @@
 instance Functor (RS s) where
     fmap f rs = rs { rules = map (fmap f) $ rules rs }
 
-strict_rules sys = 
+strict_rules sys =
     do u <- rules sys ; guard $ strict u ; return ( lhs u, rhs u )
-weak_rules sys = 
+weak_rules sys =
     do u <- rules sys ; guard $ weak u ; return ( lhs u, rhs u )
-equal_rules sys = 
+equal_rules sys =
     do u <- rules sys ; guard $ equal u ; return ( lhs u, rhs u )
 
 type TRS v s = RS s ( Term v s )
 
 type SRS s = RS s [ s ]
 
-data Problem v s = 
-     Problem { type_ :: Type 
+data Problem v s =
+     Problem { type_ :: Type
              , trs :: TRS v s
              , strategy :: Maybe Strategy
+             , full_signature :: Signature
              -- , metainformation :: Metainformation
-             , startterm :: Maybe Startterm  
+             , startterm :: Maybe Startterm
              , attributes :: Attributes
              }
 
 data Type = Termination | Complexity
-     deriving Show 
+     deriving Show
 
 data Strategy = Full | Innermost | Outermost
      deriving Show
 
-data Startterm = 
+-- | this is modelled after
+-- https://www.lri.fr/~marche/tpdb/format.html
+data Theorydecl v s
+  = Property Theory [ s ] -- ^ example: "(AC plus)"
+  | Equations [ Rule (Term v s) ]
+    deriving Typeable
+
+data Theory = A | C | AC
+  deriving (Eq, Ord, Read, Show, Typeable)
+
+data Startterm =
        Startterm_Constructor_based
        | Startterm_Full
-     deriving Show     
+     deriving Show
 
 ------------------------------------------------------
 
@@ -95,10 +129,10 @@
 mkunary   s = mk 1 s
 
 from_strict_rules :: Bool -> [(t,t)] -> RS i t
-from_strict_rules sep rs = 
+from_strict_rules sep rs =
     RS { rules = map ( \ (l,r) ->
              Rule { relation = Strict, top = False, lhs = l, rhs = r } ) rs
-       , separate = sep 
+       , separate = sep
        }
 
 with_rules sys rs = sys { rules = rs }
diff --git a/src/TPDB/Data/Attributes.hs b/src/TPDB/Data/Attributes.hs
--- a/src/TPDB/Data/Attributes.hs
+++ b/src/TPDB/Data/Attributes.hs
@@ -4,7 +4,7 @@
 
 import TPDB.Data.Term
 import TPDB.Data.Rule
-import TPDB.Pretty 
+import TPDB.Pretty
 
 import qualified Data.Set as S
 import qualified Data.Map.Strict as M
@@ -19,8 +19,9 @@
   , right_linear :: Bool
   , linear :: Bool
   , max_var_count :: Int
-  , max_var_depth :: Int
+  , max_var_depth :: Int -- ^ value is meaningless if the system has no variables
   }
+  deriving Show
 
 instance Pretty Attributes where
   pretty a = "Attributes" <+> braces ( fsep $ punctuate comma
@@ -35,8 +36,8 @@
        , "max_var_count =" <+> pretty (max_var_count a)
        , "max_var_depth =" <+> pretty (max_var_depth a)
        ] )
-  
 
+
 compute_attributes
   :: (Ord v, Ord c)
   => [Rule (Term v c)] -> Attributes
@@ -49,20 +50,23 @@
       vcs = map varcount us
   in Attributes
      { size_of_signature = S.size sig
-     , max_arity = maximum $ do
+     , max_arity = safe_maximum (-1) $ do
        u <- us ; t <- [lhs u, rhs u]
        Node f args <- subterms t
        return $ length args
      , total_term_size = sum term_sizes
-     , max_term_size = maximum term_sizes
-     , max_term_depth = maximum term_depths
+     , max_term_size = safe_maximum (-1) term_sizes
+     , max_term_depth = safe_maximum (-1) term_depths
      , left_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l <= 1
      , right_linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ r <= 1
      , linear = and $ do vc <- vcs ; (k,(l,r)) <- M.toList vc ; return $ l == 1 && r == 1 -- FIXME: or (l == r) ?
-     , max_var_count = maximum $ map M.size vcs
-     , max_var_depth = maximum $ map length $ terms >>= varpos
+     , max_var_count = safe_maximum (-1) $ map M.size vcs
+     , max_var_depth = safe_maximum (-1) $ map length $ terms >>= varpos
      }
 
+safe_maximum x [] = x
+safe_maximum x ys = maximum ys
+
 varcount :: Ord v => Rule (Term v c) -> M.Map v (Int,Int)
 varcount u = M.mergeWithKey ( \ k l r -> Just (l,r)) ( M.map ( \k -> (k,0))) (M.map ( \k -> (0,k)))
         (varcount_term $ lhs u) (varcount_term $ rhs u)
@@ -71,4 +75,3 @@
 varcount_term t = M.fromListWith (+) $ do
   (p, Var v) <- positions t
   return (v, 1)
-  
diff --git a/src/TPDB/XTC/Read.hs b/src/TPDB/XTC/Read.hs
--- a/src/TPDB/XTC/Read.hs
+++ b/src/TPDB/XTC/Read.hs
@@ -39,7 +39,7 @@
     gs <- listA ( getTerm <<< gotoChild "arg" ) -< sub
     let c = mk (length gs) nm
     returnA -< Node c gs
-          
+
 gotoChild tag = proc x -> do
     returnA <<< getChildren <<< getChild tag -< x
 
@@ -51,9 +51,11 @@
     rs <- getTRS <<< getChild "trs" -< x
     st <- getStrategy <<< getChild "strategy" -< x
     stt <- listA ( getStartterm <<< getChild "startterm" ) -< x
+    sig <- getSignature <<<  getChild "trs" -< x
     returnA -< Problem { trs = rs
                         , TPDB.Data.strategy = st
-                        , type_ = ty 
+                        , TPDB.Data.full_signature = sig
+                        , type_ = ty
                         , startterm = case stt of
                              [] -> Nothing
                              [x] -> x
@@ -79,25 +81,40 @@
    ) <+> ( proc x -> do returnA -< Nothing )
 
 getTRS = proc x -> do
-    sig <- getSignature <<< getChild "signature" -< x
+    sig <- getSignature -< x
     str <- getRules Strict <<< getChild "rules" -< x
     nostr <- listA ( getRules Weak <<< getChild "relrules" <<< getChild "rules" ) -< x
     -- FIXME: check that symbols are use with correct arity
-    th <- listA ( atTag "theory" ) -< x
-    returnA -< case th of
-        [] -> RS { signature = sig
+    returnA -< RS { signature = case sig of
+                       Signature fs -> do f <- fs ; return $ mk (fs_arity f) (fs_name f)
+                       HigherOrderSignature {} -> []
                   , rules = str ++ concat nostr
                   , separate = False -- for TRS, don't need comma between rules
                   }
-        _  -> error $ unwords [ "cannot handle theories" ]
 
-getSignature = proc x -> do
-    returnA <<< listA ( getFuncsym <<< getChild "funcsym" ) -< x
+getSignature =
+      ( getFOSignature <<< getChild "signature" )
+  <+> ( getHOSignature <<< getChild "higherOrderSignature" )
 
+getFOSignature = proc x -> do
+    fs <- listA ( getFuncsym <<< getChild "funcsym" ) -< x
+    returnA -< Signature fs
+
+getHOSignature = proc x -> do
+    returnA -< HigherOrderSignature
+
 getFuncsym = proc x -> do
     nm <- getText <<< gotoChild "name" -< x
-    ar <- getText <<< gotoChild "arity" -< x
-    returnA -< mk (read ar) nm
+    ar <- getRead <<< gotoChild "arity" -< x
+    th <- listA ( getRead <<< gotoChild "theory" ) -< x
+    rm <- listA ( listA (getRead <<< gotoChild "entry") <<< gotoChild "replacementmap" ) -< x
+    returnA -< Funcsym  { fs_name = nm
+                        , fs_arity = ar
+                        , fs_theory = case th of [] -> Nothing ; [t] -> Just t
+                        , fs_replacementmap = case rm of [] -> Nothing ; [r] -> Just (Replacementmap r)
+                        }
+
+getRead = proc x -> do s <- getText -< x ; returnA -< read s
 
 getRules str = proc x -> do
     returnA <<< listA ( getRule str  <<< getChild "rule" ) -< x
diff --git a/test/read_print_xml_theory.hs b/test/read_print_xml_theory.hs
new file mode 100644
--- /dev/null
+++ b/test/read_print_xml_theory.hs
@@ -0,0 +1,11 @@
+import TPDB.Data
+import TPDB.Pretty
+import TPDB.XTC
+import TPDB.Plain.Write
+
+import Control.Monad ( forM, void )
+
+main = void $ do
+    [ p ] <- readProblems "test/AC09.xml"
+    print $ pretty p
+    print $ full_signature p
diff --git a/tpdb.cabal b/tpdb.cabal
--- a/tpdb.cabal
+++ b/tpdb.cabal
@@ -1,5 +1,5 @@
 Name: tpdb
-Version: 1.3.2
+Version: 1.3.3
 Author: Alexander Bau, Johannes Waldmann
 Maintainer: Johannes Waldmann
 Category: Logic
@@ -88,3 +88,10 @@
   Type: exitcode-stdio-1.0
   main-is: attributes.hs
   hs-source-dirs: test 
+
+Test-Suite XML-Theory
+  Build-Depends: base==4.*, tpdb
+  Type: exitcode-stdio-1.0
+  main-is: read_print_xml_theory.hs
+  hs-source-dirs: test 
+