diff --git a/Control/CP/ComposableTransformers.hs b/Control/CP/ComposableTransformers.hs
--- a/Control/CP/ComposableTransformers.hs
+++ b/Control/CP/ComposableTransformers.hs
@@ -25,7 +25,7 @@
 solve :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,
           Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) 
       => q -> c -> Tree solver (CForResult c) -> (Int,[CForResult c])
-solve q c model = runSM $ eval model q (TStack c)
+solve q c model = run $ eval model q (TStack c)
 
 --------------------------------------------------------------------------------
 -- COMPOSABLE TRANSFORMERS
@@ -256,7 +256,7 @@
   type ForResult (RestartST es ts solver a) = a
   initT  (RestartST (c:cs) _) tree  = 
  	let (es,ts) = initCT c
-        in do l <-  markSM
+        in do l <-  mark
 	      return ((c,cs,es,l,tree),ts)
   leftT  _ (c,_,_,_,_)      = leftCT c
   rightT _ (c,_,_,_,_)      = rightCT c
diff --git a/Control/CP/FD/FD.hs b/Control/CP/FD/FD.hs
--- a/Control/CP/FD/FD.hs
+++ b/Control/CP/FD/FD.hs
@@ -36,15 +36,14 @@
 
 instance Solver FD where
   type Constraint FD  = FD_Constraint
-  type Term       FD  = FD_Term
   type Label      FD  = FDState
-
-  newvarSM 	= newVar () >>= return . FD_Var 
-  addSM    	= addFD
-  runSM p   	= runFD p
+  add    	= addFD
+  run p   	= runFD p
+  mark	= get
+  goto	= put 
 
-  markSM	= get
-  gotoSM	= put 
+instance Term FD FD_Term where
+  newvar 	= newVar () >>= return . FD_Var 
 
 data FD_Term where
   FD_Var :: FDVar -> FD_Term
diff --git a/Control/CP/FD/FDSugar.hs b/Control/CP/FD/FDSugar.hs
--- a/Control/CP/FD/FDSugar.hs
+++ b/Control/CP/FD/FDSugar.hs
@@ -43,7 +43,7 @@
 newBound :: NewBound FD
 newBound = do obj <- fd_objective
               (val:_) <- fd_domain obj 
-	      l <- markSM
+	      l <- mark
               return ((\tree -> tree `insertTree` (obj @< val)) :: forall b . Tree FD b -> Tree FD b)
 
 newBoundBis :: NewBound FD 
@@ -55,12 +55,12 @@
 restart :: (Queue q, Solver solver, CTransformer c, CForSolver c ~ solver,
           Elem q ~ (Label solver,Tree solver (CForResult c),CTreeState c)) 
       => q -> [c] -> Tree solver (CForResult c) -> (Int,[CForResult c])
-restart q cs model = runSM $ eval model q (RestartST (map Seal cs) return)
+restart q cs model = run $ eval model q (RestartST (map Seal cs) return)
 
 restartOpt :: (Queue q, CTransformer c, CForSolver c ~ FD,
           Elem q ~ (Label FD,Tree FD (CForResult c),CTreeState c)) 
       => q -> [c] -> Tree FD (CForResult c) -> (Int,[CForResult c])
-restartOpt q cs model = runSM $ eval model q (RestartST (map Seal cs) opt)
+restartOpt q cs model = run $ eval model q (RestartST (map Seal cs) opt)
 	where opt tree = newBound >>= \f -> return (f tree)
 
 --------------------------------------------------------------------------------
diff --git a/Control/CP/Herbrand/Herbrand.hs b/Control/CP/Herbrand/Herbrand.hs
--- a/Control/CP/Herbrand/Herbrand.hs
+++ b/Control/CP/Herbrand/Herbrand.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE PatternGuards #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleContexts #-}
 module Control.CP.Herbrand.Herbrand where 
 
 import Control.Monad.State.Lazy
@@ -19,7 +22,7 @@
   isVar    :: t   -> Maybe VarId
   children :: t -> ([t], [t] -> t)
   nonvar_unify
-        :: t -> t -> Herbrand t Bool
+        :: (MonadState (HState t) m) => t -> t -> m Bool
 
 -- Herbrand monad
 
@@ -42,26 +45,28 @@
                        ,subst      :: Subst t
                        }
 
-updateState :: HTerm t => (HState t -> HState t) -> Herbrand t ()
+updateState :: (HTerm t, MonadState (HState t) m) => (HState t -> HState t) -> m ()
 updateState f = get >>= put . f
 
 -- Solver instance 
 
 instance HTerm t => Solver (Herbrand t) where
-  type Term       (Herbrand t)  = t
   type Constraint (Herbrand t)  = Unify t 
   type Label      (Herbrand t)  = HState t
-  newvarSM  = newvarH
-  addSM     = addH
-  markSM    = get
-  gotoSM    = put
-  runSM     = flip evalState initState . unH
+  add     = addH
+  mark    = get
+  goto    = put
+  run     = flip evalState initState . unH
 
+instance HTerm t => Term (Herbrand t) t where
+  newvar  = newvarH
+
+
 initState = HState 0 Data.Map.empty
 
 -- New variable
 
-newvarH :: HTerm t => Herbrand t t
+newvarH :: (HTerm t,MonadState (HState t) m) => m t
 newvarH = do state <- get
              let varid = var_supply state
              put state{var_supply = varid + 1}
@@ -71,9 +76,10 @@
 
 data Unify t = t `Unify` t
 
+addH :: (HTerm t, MonadState (HState t) m) => Unify t -> m Bool
 addH (Unify t1 t2) = unify t1 t2
 
-unify :: HTerm t => t -> t -> Herbrand t Bool
+unify :: (HTerm t, MonadState (HState t) m) => t -> t -> m Bool
 unify t1 t2 = 
   do nt1 <- shallow_normalize t1
      nt2 <- shallow_normalize t2
@@ -84,16 +90,16 @@
        (_      , Just v2) -> bind v2 nt1 >> success
        (_      , _      ) -> nonvar_unify nt1 nt2
 
-success, failure :: HTerm t => Herbrand t Bool
+success, failure :: Monad m => m Bool
 success  = return True
 failure  = return False
 
-bind :: HTerm t => VarId -> t -> Herbrand t ()
+bind :: (HTerm t, MonadState (HState t) m) => VarId -> t -> m ()
 bind v t  = updateState $ \state -> state{subst = insert v t (subst state)}
 
 -- Normalization
 
-shallow_normalize :: HTerm t => t -> Herbrand t t
+shallow_normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
 shallow_normalize t
   | Just v <- isVar t    
      = do state <- get
@@ -103,11 +109,11 @@
   | otherwise  
      = return t
 
-normalize :: HTerm t => t -> Herbrand t t
+normalize :: (HTerm t, MonadState (HState t) m) => t -> m t
 normalize t
   | Just v <- isVar t  = do state <- get
                             case Data.Map.lookup v (subst state) of
                               Just t' -> normalize t'
                               Nothing -> return t
   | otherwise          = let (ts,mkt)  = children t
-                         in pure mkt <*> mapM normalize ts
+                         in mapM normalize ts >>= return . mkt
diff --git a/Control/CP/Herbrand/HerbrandT.hs b/Control/CP/Herbrand/HerbrandT.hs
new file mode 100644
--- /dev/null
+++ b/Control/CP/Herbrand/HerbrandT.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+-- |This module provides a Herbrand solver as a monad transformer.
+--
+--  The constraints offered are "Either (Unify t) (Constraint m)"
+--  where "m" is the transformed solver. Hence, both unification
+--  and the underlying solver's constraints are available.
+--
+--  The terms offered are "L t1" where "t1" is the Herbrand solver's
+--  terms and "R t2" where "t2" are the underlying solver's types.
+--  
+module Control.CP.Herbrand.HerbrandT where
+
+import Control.Monad.Trans
+import Control.Monad.State.Lazy
+
+import Control.CP.Solver
+import Control.CP.Herbrand.Herbrand (HState, Unify, HTerm,initState,addH,newvarH)
+
+newtype HerbrandT t m a = HerbrandT { unHT :: StateT (HState t) m a }
+  deriving (MonadTrans, Monad, MonadState (HState t))
+
+instance (Solver s, HTerm t) => Solver (HerbrandT t s) where
+  type Constraint (HerbrandT t s)  = Either (Unify t) (Constraint s)
+  type Label      (HerbrandT t s)  = (HState t, Label s)
+  add (Left  c)  = addH c
+  add (Right c)  = lift $ add c
+  mark           = do l <- get
+                      r <- lift $ mark
+                      return (l,r)
+  goto (l,r)     = put l >> (lift $ goto r)
+  run            = run . flip evalStateT initState . unHT
+
+data L a = L a
+data R a = R a
+
+instance (HTerm t, Solver s) => Term (HerbrandT t s) (L t) where
+  newvar  = newvarH >>= return . L 
+
+instance (HTerm t, Solver s, Term s st) => Term (HerbrandT t s) (R st) where
+  newvar  = lift newvar >>= return . R
diff --git a/Control/CP/SearchTree.hs b/Control/CP/SearchTree.hs
--- a/Control/CP/SearchTree.hs
+++ b/Control/CP/SearchTree.hs
@@ -16,13 +16,13 @@
 ----------------------------------- Tree --------------------------------------
 -------------------------------------------------------------------------------
 
-data Tree s a
- 		= Fail                          -- failure
-                | Return a                      -- finished
-                | Try (Tree s a) (Tree s a)     -- disjunction
-                | Add (Constraint s) (Tree s a) -- sequentially adding a constraint to a tree
-                | NewVar (Term s -> Tree s a)   -- add a new variable to a tree
-	        | Label (s (Tree s a))      	-- label with a strategy
+data Tree s a where
+  Fail    :: Tree s a                                  -- failure
+  Return  :: a -> Tree s a                             -- finished
+  Try     :: Tree s a -> Tree s a -> Tree s a          -- disjunction
+  Add     :: Constraint s -> Tree s a -> Tree s a      -- sequentially adding a constraint to a tree
+  NewVar  :: Term s t => (t -> Tree s a) -> Tree s a   -- add a new variable to a tree
+  Label   :: s (Tree s a) -> Tree s a      	       -- label with a strategy
 
 instance Show (Tree s a)  where
   show Fail 		= "Fail"
@@ -154,15 +154,15 @@
                                     in  (a:cs,bs)
                  in  Try (disj2 xs) (disj2 ys)
  
-exists :: (Term s -> Tree s a) -> Tree s a
+exists :: Term s t => (t -> Tree s a) -> Tree s a
 exists f = NewVar f
 
-exist :: Solver s => Int -> ([Term s] -> Tree s a) -> Tree s a
+exist :: (Solver s, Term s t) => Int -> ([t] -> Tree s a) -> Tree s a
 exist n ftree = f n []
          where f 0 acc  = ftree acc
                f n acc  = exists $ \v -> f (n-1) (v:acc)
 
-forall :: Solver s => [Term s] -> (Term s -> Tree s ()) -> Tree s ()
+forall :: (Solver s, Term s t)  => [t] -> (t -> Tree s ()) -> Tree s ()
 forall list ftree = conj $ map ftree list
  
 label :: Solver s => s (Tree s a) -> Tree s a
diff --git a/Control/CP/Solver.hs b/Control/CP/Solver.hs
--- a/Control/CP/Solver.hs
+++ b/Control/CP/Solver.hs
@@ -11,18 +11,20 @@
 class Monad solver => Solver solver where
 	-- the constraints
 	type Constraint solver 	:: *
-	-- the terms
-	type Term solver 	:: *
  	-- the labels
 	type Label solver	:: *
-	-- produce a fresh constraint variable
-	newvarSM 	:: solver (Term solver)
 	-- add a constraint to the current state, and
 	-- return whethe the resulting state is consistent
-	addSM		:: Constraint solver -> solver Bool
+	add		:: Constraint solver -> solver Bool
 	-- run a computation
-	runSM		:: solver a -> a
+	run		:: solver a -> a
 	-- mark the current state, and return its label
-	markSM		:: solver (Label solver)
+	mark		:: solver (Label solver)
 	-- go to the state with given label
-	gotoSM		:: Label solver -> solver ()
+	goto		:: Label solver -> solver ()
+
+class Solver solver => Term solver term where
+	-- produce a fresh constraint variable
+	newvar 	:: solver term
+  
+
diff --git a/Control/CP/Transformers.hs b/Control/CP/Transformers.hs
--- a/Control/CP/Transformers.hs
+++ b/Control/CP/Transformers.hs
@@ -25,13 +25,13 @@
 eval' :: SearchSig solver q t (ForResult t) 
 eval' i (Return x) wl t es ts  = do (j,xs) <- returnT (i+1) wl t es
                                     return (j,(x:xs)) 
-eval' i (Add c k)  wl t es ts = do b <- addSM c 
+eval' i (Add c k)  wl t es ts = do b <- Control.CP.Solver.add c 
                                    if b then eval' (i+1) k wl t es ts
                                         else continue (i+1) wl t es
-eval' i (NewVar f) wl t es ts = do v <- newvarSM 
+eval' i (NewVar f) wl t es ts = do v <- newvar 
                                    eval' (i+1) (f v) wl t es ts
 eval' i (Try l r)  wl t es ts  = 
-  do now <- markSM 
+  do now <- mark 
      let wl' = pushQ (now,l,leftT t es ts) $ pushQ (now,r,rightT t es ts) wl
      continue (i+1) wl' t es
 eval' i Fail       wl t es ts  = continue (i+1) wl t es
@@ -42,7 +42,7 @@
 continue i wl t es  
 	| isEmptyQ wl  = endT i wl t es -- return (i,[])
         | otherwise    = let ((past,tree,ts),wl') = popQ wl
-                         in  do gotoSM past
+                         in  do goto past
                                 nextT i tree wl' t es ts 
 
 --------------------------------------------------------------------------------
diff --git a/monadiccp.cabal b/monadiccp.cabal
--- a/monadiccp.cabal
+++ b/monadiccp.cabal
@@ -1,5 +1,5 @@
 Name:                monadiccp
-Version:             0.3
+Version:             0.4
 Description:         Monadic Constraint Programming framework
 License:             BSD3
 License-file:        LICENSE
@@ -7,7 +7,7 @@
 Maintainer:          tom.schrijvers@cs.kuleuven.be
 Build-Depends:       base, containers, mtl, haskell98, random
 Build-Type:          Simple
-Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm
+Exposed-modules:     Control.CP.ComposableTransformers  Control.CP.PriorityQueue  Control.CP.Queue  Control.CP.Solver  Control.CP.SearchTree  Control.CP.Transformers Control.CP.FD.Domain Control.CP.FD.FD Control.CP.FD.FDSugar Control.CP.Herbrand.Herbrand Control.CP.Herbrand.PrologTerm Control.CP.Herbrand.HerbrandT
 ghc-options:         
 Category:            control
 Synopsis:	     Package for Constraint Programming