diff --git a/src/Term/LTerm.hs b/src/Term/LTerm.hs
--- a/src/Term/LTerm.hs
+++ b/src/Term/LTerm.hs
@@ -99,9 +99,6 @@
   , module Term.VTerm
 ) where
 
-import           Term.Rewriting.Definitions
-import           Term.VTerm
-
 import           Text.PrettyPrint.Class
 
 import           Control.Applicative
@@ -126,8 +123,12 @@
 import           Extension.Data.Monoid
 import           Extension.Prelude
 
+
 import           Logic.Connectives
 
+import           Term.Rewriting.Definitions
+import           Term.VTerm
+
 ------------------------------------------------------------------------------
 -- Sorts.
 ------------------------------------------------------------------------------
@@ -278,6 +279,10 @@
 isFreshVar :: LNTerm -> Bool
 isFreshVar (viewTerm -> Lit (Var v)) = (lvarSort v == LSortFresh)
 isFreshVar _                         = False
+
+
+-- Utility functions for constraint solving
+-------------------------------------------
 
 -- | The non-inverse factors of a term.
 niFactors :: LNTerm -> [LNTerm]
diff --git a/src/Term/Rewriting/Norm.hs b/src/Term/Rewriting/Norm.hs
--- a/src/Term/Rewriting/Norm.hs
+++ b/src/Term/Rewriting/Norm.hs
@@ -15,13 +15,6 @@
   , maybeNotNfSubterms
 ) where
 
-import           Term.LTerm
-import           Term.Maude.Process
-import           Term.Maude.Signature
-import           Term.Substitution
-import           Term.SubtermRule
-import           Term.Unification
-
 import           Utils.Misc
 
 import           Control.Basics
@@ -31,6 +24,14 @@
 import qualified Data.Set             as S
 
 import           System.IO.Unsafe     (unsafePerformIO)
+
+
+import           Term.LTerm
+import           Term.Maude.Process
+import           Term.Maude.Signature
+import           Term.Substitution
+import           Term.SubtermRule
+import           Term.Unification
 
 ----------------------------------------------------------------------
 -- Normalization using Maude
diff --git a/src/Term/Term.hs b/src/Term/Term.hs
--- a/src/Term/Term.hs
+++ b/src/Term/Term.hs
@@ -76,8 +76,8 @@
 import qualified Data.ByteString.Char8 as BC
 import           Extension.Data.ByteString ()
 
-
 import           Text.PrettyPrint.Class
+
 import           Term.Term.Classes
 import           Term.Term.FunctionSymbols
 import           Term.Term.Raw
diff --git a/src/Term/Term/Raw.hs b/src/Term/Term/Raw.hs
--- a/src/Term/Term/Raw.hs
+++ b/src/Term/Term/Raw.hs
@@ -82,7 +82,7 @@
 fApp (AC acSym)  ts = fAppAC acSym ts
 fApp (C o)       ts = fAppC o ts
 fApp List        ts = FAPP List ts
-fApp s@(NoEq _) ts = FAPP s ts
+fApp s@(NoEq _)  ts = FAPP s ts
 
 -- | Smart constructor for AC terms.
 fAppAC :: Ord a => ACSym -> [Term a] -> Term a
@@ -97,11 +97,11 @@
     (o_as0, non_o_as) = partition isOTerm as
     o_as              = [ a | FAPP _ ts <- o_as0, a <- ts ]
 
--- | Smart constructor for AC terms.
+-- | Smart constructor for C terms.
 fAppC :: Ord a => CSym -> [Term a] -> Term a
 fAppC nacsym as = FAPP (C nacsym) (sort as)
 
--- | Smart constructor for non-AC terms.
+-- | Smart constructor for non-AC/C terms.
 {-# INLINE fAppNoEq #-}
 fAppNoEq :: NoEqSym -> [Term a] -> Term a
 fAppNoEq freesym = FAPP (NoEq freesym)
diff --git a/src/Term/Unification.hs b/src/Term/Unification.hs
--- a/src/Term/Unification.hs
+++ b/src/Term/Unification.hs
@@ -68,6 +68,7 @@
 
 import           System.IO.Unsafe (unsafePerformIO)
 
+
 import           Term.Rewriting.Definitions
 import           Term.Substitution
 import qualified Term.Maude.Process as UM
@@ -75,7 +76,6 @@
                    (MaudeHandle, WithMaude, startMaude, getMaudeStats, mhMaudeSig, mhFilePath)
 import           Term.Maude.Signature
 import           Debug.Trace.Ignore
--- import qualified Debug.Trace as DT
 
 -- Unification modulo AC
 ----------------------------------------------------------------------
@@ -112,7 +112,6 @@
 
 -- | @unifyLNTerm eqs@ returns a complete set of unifiers for @eqs@ modulo AC.
 unifyLNTerm :: [Equal LNTerm] -> WithMaude [SubstVFresh Name LVar]
--- unifyLNTerm eqs = reader $ \hnd -> (\res -> DT.trace (show ("unify", res, eqs)) res) $ unifyLTerm sortOfName eqs `runReader` hnd
 unifyLNTerm = unifyLTerm sortOfName
 
 -- | 'True' iff the terms are unifiable.
@@ -121,7 +120,8 @@
 
 -- | Flatten a factored substitution to a list of substitutions.
 flattenUnif :: IsConst c => (LSubst c, [LSubstVFresh c]) -> [LSubstVFresh c]
-flattenUnif (subst, substs) =  (\res -> trace (show ("flattenUnif",subst, substs,res )) res) $ map (`composeVFresh` subst) substs
+flattenUnif (subst, substs) = 
+    (\res -> trace (show ("flattenUnif",subst, substs,res )) res) $ map (`composeVFresh` subst) substs
 
 -- Matching modulo AC
 ----------------------------------------------------------------------
diff --git a/tamarin-prover-term.cabal b/tamarin-prover-term.cabal
--- a/tamarin-prover-term.cabal
+++ b/tamarin-prover-term.cabal
@@ -2,7 +2,7 @@
 
 cabal-version:      >= 1.8
 build-type:         Simple
-version:            0.8.5.0
+version:            0.8.5.1
 license:            GPL
 license-file:       LICENSE
 category:           Theorem Provers
@@ -58,7 +58,7 @@
 
       , HUnit                == 1.*
 
-      , tamarin-prover-utils >= 0.8.5  && < 0.9
+      , tamarin-prover-utils >= 0.8.5.1  && < 0.9
 
 
     hs-source-dirs: src