diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,6 +1,6 @@
 Name:          cflp
-Version:       0.2.2
-Cabal-Version: >= 1.2
+Version:       0.2.5
+Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
                functional-logic programming ((C)FLP) in Haskell. The 
@@ -13,6 +13,7 @@
 License-File:  LICENSE
 Author:        Sebastian Fischer
 Maintainer:    sebf@informatik.uni-kiel.de
+Bug-Reports:   mailto:sebf@informatik.uni-kiel.de
 Homepage:      http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html
 Build-Type:    Custom
 Stability:     alpha
@@ -20,10 +21,15 @@
 Extra-Source-Files: README, INSTALL, Makefile, configure, Test.lhs
 
 Library
-  Build-Depends:    base >= 4, ghc, mtl, syb, HUnit
+  Build-Depends:    base >= 4, 
+                    containers, 
+                    value-supply >= 0.3, 
+                    mtl, 
+                    syb, 
+                    HUnit
   Exposed-Modules:  Control.CFLP
-  Other-Modules:    Control.Monad.Constraint,
-                    Control.Monad.Constraint.Choice,
+  Other-Modules:    Control.Monad.Update,
+                    Control.Constraint.Choice,
                     Data.LazyNondet,
                     Data.LazyNondet.Types,
                     Data.LazyNondet.Types.Bool,
@@ -35,7 +41,7 @@
                     Control.CFLP.Tests,
                     Control.CFLP.Tests.CallTimeChoice
   Hs-Source-Dirs:   src
-  Extensions:       ExistentialQuantification,
+  Extensions:       FunctionalDependencies,
                     MultiParamTypeClasses,
                     FlexibleInstances,
                     FlexibleContexts,
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
--- a/src/Control/CFLP.lhs
+++ b/src/Control/CFLP.lhs
@@ -24,36 +24,32 @@
 > ) where
 >
 > import Data.LazyNondet
-> import Data.LazyNondet.Primitive
 > import Data.LazyNondet.Types.Bool
 > import Data.LazyNondet.Types.List
 >
 > import Control.Monad.State
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
-> class (MonadConstr Choice m,
->        ConstraintStore Choice cs,
->        ChoiceStore cs,
->        MonadSolve cs m m)
->  => CFLP cs m
+> import Control.Constraint.Choice
+>
+> class (MonadUpdate s m, Update s m m, ChoiceStore s) => CFLP s m
 
 The type class `CFLP` is a shortcut for the type-class constraints on
 constraint functional-logic computations that are parameterized over a
 constraint store and a constraint monad. Hence, such computations can
 be executed with different constraint stores and search strategies.
 
-> instance CFLP ChoiceStoreUnique (ConstrT ChoiceStoreUnique [])
+> instance CFLP ChoiceStoreIM (UpdateT ChoiceStoreIM [])
 
 We declare instances for every combination of monad and constraint
 store that we intend to use.
 
-> type CS = ChoiceStoreUnique
+> type CS = ChoiceStoreIM
 >
 > noConstraints :: CS
 > noConstraints = noChoices
 >
-> type Computation m a = CS -> ID -> Nondet CS (ConstrT CS m) a
+> type Computation m a = CS -> ID -> Nondet CS (UpdateT CS m) a
 
 Currently, the constraint store used to evaluate constraint
 functional-logic programs is simply a `ChoiceStore`. It will be a
@@ -70,7 +66,7 @@
 
 The strategy of the list monad is depth-first search.
 
-> evaluate :: (CFLP CS m, MonadSolve CS m m')
+> evaluate :: (CFLP CS m, Update CS m m')
 >          => (Nondet CS m a -> CS -> m' b)
 >          -> Strategy m' -> (CS -> ID -> Nondet CS m a)
 >          -> IO [b]
@@ -81,17 +77,16 @@
 The `evaluate` function enumerates the non-deterministic solutions of a
 constraint functional-logic computation according to a given strategy.
 
-> eval, evalPartial :: (CFLP CS m, MonadSolve CS m m', Data a)
+> eval, evalPartial :: (CFLP CS m, Update CS m m', Data a)
 >                   => Strategy m' -> (CS -> ID -> Nondet CS m a)
 >                   -> IO [a]
 > eval        s = liftM (map prim) . evaluate groundNormalForm  s
 > evalPartial s = liftM (map prim) . evaluate partialNormalForm s
 >
-> evalPrint :: (CFLP CS m, MonadSolve CS m m', Data a, Show a)
+> evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a)
 >           => Strategy m' -> (CS -> ID -> Nondet CS m a)
 >           -> IO ()
-> evalPrint s op = eval s op >>= printSols
->  -- evaluate partialNormalForm s op >>= printSols
+> evalPrint s op = evaluate partialNormalForm s op >>= printSols
 >
 > printSols :: Show a => [a] -> IO ()
 > printSols []     = putStrLn "No more solutions."
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
--- a/src/Control/CFLP/Tests/CallTimeChoice.lhs
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -34,7 +34,7 @@
 >
 > ignot :: CFLP cs m
 >       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool
-> ignot _ x = not x
+> ignot _ = not
 
 This test checks a function with two arguments, where the first must
 be ignored. Any changes in the translation scheme must not lead to
@@ -45,7 +45,7 @@
 > sharedVarsAreEqual :: Assertion
 > sharedVarsAreEqual = assertResults comp [[False,False],[True,True]]
 >  where
->   comp _ u = two (unknown u)
+>   comp _ = two . unknown
 >
 > two :: Monad m => Nondet cs m a -> Nondet cs m [a]
 > two x = x ^: x ^: nil
diff --git a/src/Control/Constraint/Choice.lhs b/src/Control/Constraint/Choice.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/Constraint/Choice.lhs
@@ -0,0 +1,78 @@
+% Sharing Choices with Constraints
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+We define a constraint store that stores choice constraints which
+ensure that shared non-deterministic choices evaluate to the same
+values when translating lazy functional logic programs.
+
+Based on this constraint store, we provide a function `choice` that
+can be used to generate choices that are constrained to evaluate to
+the same value if they are shared.
+
+> {-# LANGUAGE
+>       MultiParamTypeClasses,
+>       FlexibleInstances,
+>       FlexibleContexts
+>   #-}
+>
+> module Control.Constraint.Choice (
+>
+>   ChoiceStore(..), ChoiceStoreIM, noChoices, choice
+>
+> ) where
+>
+> import Control.Monad.State
+> import Control.Monad.Update
+>
+> import qualified Data.IntMap as IM
+>
+> class ChoiceStore s
+>  where
+>   lookupChoice :: Int -> s -> Maybe Int
+>   assertChoice :: MonadPlus m => s -> Int -> Int -> s -> m s
+
+We define an interface for choice stores that provide an operation to
+lookup a previously made choice. The first argument of `assertChoice`
+is a dummy argument to fix the type of the store in partial
+applications.
+
+
+> newtype ChoiceStoreIM = ChoiceStoreIM (IM.IntMap Int) deriving Show
+>
+> noChoices :: ChoiceStoreIM
+> noChoices = ChoiceStoreIM IM.empty
+>
+> instance ChoiceStore ChoiceStoreIM
+>  where
+>   lookupChoice u (ChoiceStoreIM cs) = IM.lookup u cs
+>
+>   assertChoice _ u x (ChoiceStoreIM cs) = do
+>     maybe (return (ChoiceStoreIM (IM.insert u x cs)))
+>           (\y -> do guard (x==y); return (ChoiceStoreIM cs))
+>           (IM.lookup u cs)
+
+A finite map mapping unique identifiers to integers is a
+`ChoiceStore`. The `assertChoice` operations fails to insert
+conflicting choices.
+
+> choice :: (MonadUpdate s m, ChoiceStore s) => s -> Int -> [m a] -> m a
+> choice cs u xs =
+>   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)
+>         (xs!!)
+>         (lookupChoice u cs)
+>  where constrain n = (update (assertChoice cs u n)>>)
+
+The operation `choice` takes a unique label and a list of monadic
+values that can be constrained with choice constraints. The result is
+a single monadic action combining the alternatives with `mplus`. If it
+occurs more than once in a bigger monadic action, the result is
+constrained to take the same alternative everywhere when collecting
+constraints.
+
+If a choice with the same label has been created previously and the
+label is already constrained to an alternative, then this alternative
+is returned directly and no choice is created.
+
+This situation occurs when a shared logic variable is renarrowed when
+it is demanded again during a computation.
+
diff --git a/src/Control/Monad/Constraint.lhs b/src/Control/Monad/Constraint.lhs
deleted file mode 100644
--- a/src/Control/Monad/Constraint.lhs
+++ /dev/null
@@ -1,170 +0,0 @@
-% Constraint Collecting Monads
-% Sebastian Fischer (sebf@informatik.uni-kiel.de)
-
-We define type classes and instances for monads that can collect
-constraints. The challenge is to define the interface such that
-instances can implement it without threading a store through monadic
-computations and shared monadic computations are evaluated only once.
-
-> {-# LANGUAGE 
->       MultiParamTypeClasses,
->       FlexibleInstances,
->       ExistentialQuantification
->   #-}
->
-> module Control.Monad.Constraint (
->
->   -- type classes
->   ConstraintStore(..), MonadConstr(..), MonadSolve(..),
->
->   -- monad transformer
->   ConstrT
->
-> ) where
-> 
-> import Control.Monad.State
-> import Control.Monad.Trans
->
-> class ConstraintStore c cs
->  where
->   assert :: (MonadState cs m, MonadPlus m) => c -> m ()
-
-Constraint Stores provide an operation to assert a constraint into a
-store. The constraint store is manipulated in an instance of
-`MonadState`. The `assert` operation may fail or branch depending on
-the given constraint or the current store and is, hence, performed in
-an instance of `MonadPlus`.
-
-A constraint store may support different types of constraints and a
-constraint may be supported by different constraint stores.
-
-> class MonadPlus m => MonadConstr c m
->  where
->   constr :: c -> m ()
-
-A monad that supports collecting constraints is an instance of the
-class `MonadConstr` that provides an operation to associate a
-constraint of type `c` to monadic computations. One monad may support
-different types of constraints and the same constraint type may be
-supported by different monads.
-
-> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (StateT cs m)
->  where
->   constr = assert
-
-An instance of `MonadPlus` that threads a constraint store can be
-constrained with constraints that are supported by the threaded store.
-
-> class (MonadPlus m, MonadPlus m') => MonadSolve cs m m'
->  where
->   solve :: m a -> StateT cs m' a
-
-We also define an interface for monads that can solve associated
-constraints by threading a constraint store through a (possibly, but
-not necessarily different) monad.
-
-We use the state monad transformer `StateT` to thread the constraint
-store through the monad that returns the results.
-
-> instance MonadPlus m => MonadSolve cs (StateT cs m) m
->  where
->   solve = id
-
-Again, a state threading monad gives rise to a natural instance, where
-results are returned in the base monad.
-
-State monads are a natural choice for a constraint monad, but they
-have a drawback: monadic values are functions that are reexecuted for
-each shared occurrence of a monadic sub computation.
-
-Shared Monadic Values
----------------------
-
-We define a monad transformer `ConstrT` that adds the capability of
-collecting and solving constraints to arbitrary instances of
-`MonadPlus`. Monadic actions in the resulting monads are data terms if
-monadic actions are data terms in the base monad. As a consequence,
-they are evaluated only once if they are shared.
-
-> newtype ConstrT cs m a = ConstrT { unConstrT :: m (WithConstr cs m a) }
-> data WithConstr cs m a
->   = Return a
->   | forall c . ConstraintStore c cs => Constr c (ConstrT cs m a)
-
-The type `c` of collected constraints is existentially quantified in
-order to allow different types of constraints in the same monadic
-action. All types of constraints that are collected in a monadic
-action need to be supported by the constraint store of type `cs`.
-
-> instance (MonadPlus m, ConstraintStore c cs) => MonadConstr c (ConstrT cs m)
->  where
->   constr c = ConstrT (return (Constr c (return ())))
-
-A transformed instance of `MonadPlus` is an instance of `MonadConstr`.
-
-> instance MonadPlus m => MonadSolve cs (ConstrT cs m) m
->  where
->   solve = run
->    where
->     run :: MonadPlus m => ConstrT cs m a -> StateT cs m a
->     run x = lift (unConstrT x) >>= constrain
->
->     constrain (Return a)   = return a
->     constrain (Constr c y) = do constr c; run y
-
-It is also an instance of `MonadSolve` where results are returned in
-the base monad. In order to eliminate stored constraints, we thread a
-constraint store through the monadic value and assert the associated
-constraints into the store.
-
-> instance MonadPlus m => MonadSolve cs (ConstrT cs m) (ConstrT cs m)
->  where
->   solve = run
->    where
->     run :: MonadPlus m => ConstrT cs m a -> StateT cs (ConstrT cs m) a
->     run x = lift (lift (unConstrT x)) >>= constrain
->
->     constrain (Return a)   = return a
->     constrain (Constr c y) = do lift (constr c); constr c; run y
-
-We define another instance of `MonadSolve` where results are not
-returned in the base monad but in the transformed base monad. This
-instance is useful to support computations that may or may not
-consider the threaded constraint store. All constraints are kept in
-the monadic values and threaded additionally.
-
-> instance Monad m => Monad (ConstrT cs m)
->  where
->   return = ConstrT . return . Return
->
->   x >>= f = ConstrT (unConstrT x >>= g)
->    where g (Return a)   = unConstrT (f a)
->          g (Constr c y) = return (Constr c (y >>= f))
->
-> instance MonadPlus m => MonadPlus (ConstrT cs m)
->  where
->   mzero       = ConstrT mzero
->   x `mplus` y = ConstrT (unConstrT x `mplus` unConstrT y)
->
-> instance MonadTrans (ConstrT cs)
->  where
->   lift x = ConstrT (x >>= return . Return)
-
-We specify that a transformed monad is indeed a monad, that it is an
-instance of `MonadPlus` if the base monad is, and that, `ConstrT`
-(with an arbitrary constraint store `cs`) is a monad transformer.
-
-> instance Show a => Show (ConstrT cs [] a)
->  where
->   show (ConstrT x) = show x
->
-> instance Show a => Show (WithConstr cs [] a)
->  where
->   show (Return x) = "(Return "++show x++")"
->   show (Constr _ (ConstrT x)) = "(Constr _ "++show x++")"
-
-To simplify debugging, we define `Show` instances for transformed list
-monads. Unfortunately, I don't know an easy way to show collected
-constraints, because their type is not determined by the constraint
-store and not mentioned in the signature of the instances.
-
diff --git a/src/Control/Monad/Constraint/Choice.lhs b/src/Control/Monad/Constraint/Choice.lhs
deleted file mode 100644
--- a/src/Control/Monad/Constraint/Choice.lhs
+++ /dev/null
@@ -1,87 +0,0 @@
-% Sharing Choices with Constraints
-% Sebastian Fischer (sebf@informatik.uni-kiel.de)
-
-We define a constraint store that stores choice constraints which
-ensure that shared non-deterministic choices evaluate to the same
-values when translating lazy functional logic programs.
-
-Based on this constraint store, we provide a function `choice` that
-can be used to generate choices that are constrained to evaluate to
-the same value if they are shared.
-
-> {-# LANGUAGE
->       MultiParamTypeClasses,
->       FlexibleInstances,
->       FlexibleContexts
->   #-}
->
-> module Control.Monad.Constraint.Choice (
->
->   Choice, ChoiceStore(..), ChoiceStoreUnique, noChoices, choice
->
-> ) where
->
-> import Control.Monad.State
-> import Control.Monad.Constraint
->
-> import Unique
-> import UniqFM
-
-We borrow unique identifiers from the package `ghc` which is hidden by
-default.
-
-> class ChoiceStore cs
->  where
->   lookupChoice :: Unique -> cs -> Maybe Int
-
-We define an interface for choice stores that provide an operation to
-lookup a previously made choice.
-
-> newtype Choice = Choice (Unique,Int)
-> newtype ChoiceStoreUnique = ChoiceStore (UniqFM Int)
->
-> noChoices :: ChoiceStoreUnique
-> noChoices = ChoiceStore emptyUFM
->
-> instance ChoiceStore ChoiceStoreUnique
->  where
->   lookupChoice u (ChoiceStore cs) = lookupUFM_Directly cs u
-
-A finite map mapping `Unique`s to integers is a `ChoiceStore`.
-
-> instance ConstraintStore Choice ChoiceStoreUnique
->  where
->   assert (Choice (u,x)) = do
->     ChoiceStore cs <- get
->     maybe (put (ChoiceStore (addToUFM_Directly cs u x)))
->           (guard . (x==))
->           (lookupUFM_Directly cs u)
-
-Choices are labeled with a `Unique`, so we can store them in a
-`UniqFM` making it an instance of `ConstraintStore`.
-
-The `assert` operations fails to insert conflicting choices.
-
-> choice :: (MonadConstr Choice m, ChoiceStore cs)
->        => cs -> Unique -> [m a] -> m a
-> choice cs u xs =
->   maybe (foldr1 mplus . (mzero:) . zipWith constrain [(0::Int)..] $ xs)
->         (xs!!)
->         (lookupChoice u cs)
->  where constrain n = (constr (Choice (u,n))>>)
-
-The operation `choice` takes a unique label and a list of monadic
-values that can be constrained with choice constraints. The result is
-a single monadic action combining the alternatives with `mplus`. If it
-occurs more than once in a bigger monadic action, the result is
-constrained to take the same alternative everywhere when collecting
-constraints.
-
-If a choice with the same label has been created previously and the
-label is already constrained to an alternative, then this alternative
-is returned directly and no choice is created.
-
-This situation may occur if a shared logic variable is renarrowed
-whenever it is demanded rather than shared and only narrowed on
-creation.
-
diff --git a/src/Control/Monad/Update.lhs b/src/Control/Monad/Update.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/Monad/Update.lhs
@@ -0,0 +1,153 @@
+% Monads with Non-Deterministically Updateable State
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+We define type classes and instances for monads that
+non-deterministically update state. The challenge is to define the
+interface such that instances can implement it without threading a
+store through monadic computations and shared monadic computations are
+evaluated only once.
+
+> {-# LANGUAGE 
+>       MultiParamTypeClasses,
+>       FlexibleInstances,
+>       FlexibleContexts,
+>       RankNTypes
+>   #-}
+>
+> module Control.Monad.Update (
+>
+>   -- type classes
+>   MonadUpdate(..), Update(..),
+>
+>   -- monad transformer
+>   UpdateT
+>
+> ) where
+> 
+> import Control.Monad.State
+> import Control.Monad.Trans
+>
+> class MonadPlus m => MonadUpdate s m
+>  where
+>   update :: (forall m' . MonadPlus m' => s -> m' s) -> m ()
+
+A monad that supports non-deterministic state updates is an instance
+of the class `MonadUpdate` that provides an operation to incorporate a
+monadic update-action into monadic computations.
+
+> instance MonadPlus m => MonadUpdate s (StateT s m)
+>  where
+>   update upd = get >>= upd >>= put
+
+An instance of `MonadPlus` that threads a state can update that state
+non-deterministically.
+
+> class (MonadPlus m, MonadPlus m') => Update s m m'
+>  where
+>   updateState :: m a -> StateT s m' a
+
+We also define an interface for monads that perform associated updates
+in a state that is threaded through a (possibly, but not necessarily
+different) monad.
+
+We use the state monad transformer `StateT` to thread the constraint
+store through the monad that returns the results.
+
+> instance MonadPlus m => Update s (StateT s m) m
+>  where
+>   updateState = id
+
+Again, a state threading monad gives rise to a natural instance, where
+results are returned in the base monad.
+
+State monads are a natural choice for a monad that updates state, but
+they have a drawback: monadic values are functions that are reexecuted
+for each shared occurrence of a monadic sub computation.
+
+Shared Monadic Values
+---------------------
+
+We define a monad transformer `UpdateT` that adds the capability of
+non-deterministic state updates to arbitrary instances of
+`MonadPlus`. Monadic actions in the resulting monads are data terms if
+monadic actions are data terms in the base monad. As a consequence,
+they are evaluated only once if they are shared.
+
+> newtype UpdateT s m a = UpdateT { unUpdateT :: m (WithUpdate s m a) }
+> data WithUpdate s m a
+>   = Return a
+>   | Update (forall m' . MonadPlus m' => s -> m' s)
+>            (UpdateT s m a)
+
+The updating monadic action must be polymorphic in the used monad
+`m'`.
+
+> instance MonadPlus m => MonadUpdate s (UpdateT s m)
+>  where
+>   update upd = UpdateT (return (Update upd (return ())))
+
+A transformed instance of `MonadPlus` is an instance of `MonadUpdate`.
+
+> instance MonadPlus m => Update s (UpdateT s m) m
+>  where
+>   updateState = run
+>    where
+>     run :: MonadPlus m => UpdateT s m a -> StateT s m a
+>     run x = lift (unUpdateT x) >>= doUpdate
+>
+>     doUpdate (Return a)     = return a
+>     doUpdate (Update upd y) = do update upd; run y
+
+It is also an instance of `Update` where results are returned in the
+base monad. In order to perform stored updates, we thread a state
+through the monadic computation.
+
+> instance MonadPlus m => Update s (UpdateT s m) (UpdateT s m)
+>  where
+>   updateState = run
+>    where
+>     run :: MonadPlus m => UpdateT s m a -> StateT s (UpdateT s m) a
+>     run x = lift (lift (unUpdateT x)) >>= doUpdate
+>
+>     doUpdate (Return a)     = return a
+>     doUpdate (Update upd y) = do lift (update upd); update upd; run y
+
+We define another instance of `Update` where results are not returned
+in the base monad but in the transformed base monad. This instance is
+useful to support computations that may or may not consider the
+threaded store. All upcate actions are kept in the monadic values and
+threaded additionally.
+
+> instance Monad m => Monad (UpdateT s m)
+>  where
+>   return = UpdateT . return . Return
+>
+>   x >>= f = UpdateT (unUpdateT x >>= g)
+>    where g (Return a)     = unUpdateT (f a)
+>          g (Update upd y) = return (Update upd (y >>= f))
+>
+> instance MonadPlus m => MonadPlus (UpdateT s m)
+>  where
+>   mzero       = UpdateT mzero
+>   x `mplus` y = UpdateT (unUpdateT x `mplus` unUpdateT y)
+>
+> instance MonadTrans (UpdateT s)
+>  where
+>   lift = UpdateT . liftM Return
+
+We specify that a transformed monad is indeed a monad, that it is an
+instance of `MonadPlus` if the base monad is, and that, `UpdateT`
+(with an arbitrary store `s`) is a monad transformer.
+
+> instance Show a => Show (UpdateT s [] a)
+>  where
+>   show (UpdateT x) = show x
+>
+> instance Show a => Show (WithUpdate cs [] a)
+>  where
+>   show (Return x) = "(Return "++show x++")"
+>   show (Update _ (UpdateT x)) = "(Update _ "++show x++")"
+
+To simplify debugging, we define `Show` instances for transformed list
+monads.
+
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
--- a/src/Data/LazyNondet.lhs
+++ b/src/Data/LazyNondet.lhs
@@ -16,7 +16,7 @@
 >
 >   withHNF, caseOf, caseOf_, Match,
 >
->   Data, nondet, groundNormalForm, partialNormalForm,
+>   Data, nondet, prim, groundNormalForm, partialNormalForm,
 >
 >   ConsRep(..), cons, match,
 >
diff --git a/src/Data/LazyNondet/Matching.lhs b/src/Data/LazyNondet/Matching.lhs
--- a/src/Data/LazyNondet/Matching.lhs
+++ b/src/Data/LazyNondet/Matching.lhs
@@ -7,8 +7,7 @@
 >       FlexibleContexts,
 >       FlexibleInstances,
 >       MultiParamTypeClasses,
->       FunctionalDependencies,
->       ExistentialQuantification
+>       FunctionalDependencies
 >   #-}
 >
 > module Data.LazyNondet.Matching (
@@ -23,23 +22,22 @@
 > import Data.LazyNondet.Types
 >
 > import Control.Monad.State
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
-> withHNF :: (Monad m, MonadSolve cs m m)
+> withHNF :: (Monad m, Update cs m m)
 >         => Nondet cs m a
 >         -> (HeadNormalForm cs m -> cs -> Nondet cs m b)
 >         -> cs -> Nondet cs m b
 > withHNF x b cs = Typed (do
->   (hnf,cs') <- runStateT (solve (untyped x)) cs
+>   (hnf,cs') <- runStateT (updateState (untyped x)) cs
 >   untyped (b hnf cs'))
 
 The `withHNF` operation can be used for pattern matching and solves
 constraints associated to the head constructor of a non-deterministic
 value. An updated constraint store is passed to the computation of the
 branch function. Collected constraints are kept attached to the
-computed value by using an appropriate instance of `MonadSolve` that
-does not eliminate them.
+computed value by using an appropriate instance of `Update` that does
+not eliminate them.
 
 > class WithUntyped a
 >  where
@@ -99,12 +97,11 @@
 function to typed versions of these values.
 
 > newtype Match a cs m b = Match { unMatch :: (ConIndex, cs -> Branch cs m b) }
-> data Branch cs m a =
->   forall t . (WithUntyped t, cs ~ C t, m ~ M t, a ~ T t) => Branch t
+> type Branch cs m a = [Untyped cs m] -> Nondet cs m a
 >
 > match :: (ConsRep a, WithUntyped b)
 >       => a -> (C b -> b) -> Match t (C b) (M b) (T b)
-> match c alt = Match (constrIndex (consRep c), Branch . alt)
+> match c alt = Match (constrIndex (consRep c), withUntyped . alt)
 
 The operation `match` is used to build destructor functions for
 non-deterministic values that can be used with `caseOf`.
@@ -114,11 +111,11 @@
 
 Failure is just a type version of `mzero`.
 
-> caseOf :: (MonadSolve cs m m, MonadConstr Choice m)
+> caseOf :: Update cs m m
 >        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b
 > caseOf x bs = caseOf_ x bs failure
 >
-> caseOf_ :: (MonadSolve cs m m, MonadConstr Choice m)
+> caseOf_ :: Update cs m m
 >         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b
 >         -> cs -> Nondet cs m b
 > caseOf_ x bs def =
@@ -129,10 +126,7 @@
 >       | p cs      -> delayed p (\cs -> caseOf_ (Typed (res cs)) bs def cs)
 >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs
 >     Cons _ idx args ->
->       maybe def (\b -> branch (b cs) args) (lookup idx (map unMatch bs))
->
-> branch :: Branch cs m a -> [Untyped cs m] -> Nondet cs m a
-> branch (Branch alt) = withUntyped alt
+>       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))
 
 We provide operations `caseOf_` and `caseOf` (with and without a
 default alternative) for more convenient pattern matching. The untyped
@@ -148,7 +142,7 @@
 >
 > instance (Monad m, Data a) => MkCons cs m a (Nondet cs m t)
 >  where
->   mkCons c args = Typed (return (mkHNF (toConstr c) (reverse args)))
+>   mkCons c = Typed . return . mkHNF (toConstr c) . reverse
 >
 > instance MkCons cs m b c => MkCons cs m (a -> b) (Nondet cs m t -> c)
 >  where
diff --git a/src/Data/LazyNondet/Narrowing.lhs b/src/Data/LazyNondet/Narrowing.lhs
--- a/src/Data/LazyNondet/Narrowing.lhs
+++ b/src/Data/LazyNondet/Narrowing.lhs
@@ -15,23 +15,24 @@
 > import Data.Maybe
 > import Data.LazyNondet.Types
 >
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
-> import UniqSupply
+> import Control.Constraint.Choice
 >
-> unknown :: (MonadConstr Choice m, Narrow cs a) => ID -> Nondet cs m a
+> import Data.Supply
+>
+> unknown :: (MonadUpdate cs m, Narrow cs a) => ID -> Nondet cs m a
 > unknown u = freeVar u (delayed (redelay u) (\cs -> narrow cs u))
 >
 > redelay :: ChoiceStore cs => ID -> cs -> Bool
-> redelay (ID us) = isNothing . lookupChoice (uniqFromSupply us)
+> redelay (ID us) = isNothing . lookupChoice (supplyValue us)
 
 The application of `unknown` to a constraint store and a unique
 identifier represents a logic variable of an arbitrary type. 
 
 > class ChoiceStore cs => Narrow cs a
 >  where
->   narrow :: MonadConstr Choice m => cs -> ID -> Nondet cs m a
+>   narrow :: MonadUpdate cs m => cs -> ID -> Nondet cs m a
 
 Logic variables of type `a` can be narrowed to head-normal form if
 there is an instance of the type class `Narrow`. A constraint store
@@ -40,7 +41,7 @@
 non-deterministic generator using `oneOf`, but for specific types
 different strategies may be implemented.
 
-> (?) :: (MonadConstr Choice m, ChoiceStore cs)
+> (?) :: (MonadUpdate cs m, ChoiceStore cs)
 >     => Nondet cs m a -> Nondet cs m a -> ID -> Nondet cs m a
 > (x ? y) u = delayed (redelay u) (\cs -> oneOf [x,y] cs u)
 
@@ -50,9 +51,9 @@
 current constraint store, the arguments of `(?)` are shared among all
 executions and *not* reexecuted.
 
-> oneOf :: (MonadConstr Choice m, ChoiceStore cs)
+> oneOf :: (MonadUpdate cs m, ChoiceStore cs)
 >       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a
-> oneOf xs cs (ID us) = Typed (choice cs (uniqFromSupply us) (map untyped xs))
+> oneOf xs cs (ID us) = Typed (choice cs (supplyValue us) (map untyped xs))
 
 The operation `oneOf` takes a list of non-deterministic values and
 returns a non-deterministic value that yields one of the elements in
diff --git a/src/Data/LazyNondet/Primitive.lhs b/src/Data/LazyNondet/Primitive.lhs
--- a/src/Data/LazyNondet/Primitive.lhs
+++ b/src/Data/LazyNondet/Primitive.lhs
@@ -18,12 +18,12 @@
 > import Data.LazyNondet.Types
 >
 > import Control.Monad.State
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
-> import Unique
-> import UniqSupply
+> import Control.Constraint.Choice
 >
+> import Data.Supply
+>
 > prim :: Data a => NormalForm -> a
 > prim (Var u) = error $ "demand on logic variable " ++ show u
 > prim (NormalForm con args) =
@@ -49,10 +49,10 @@
 We also provide a generic operation `nondet` to translate instances of
 the `Data` class into non-deterministic data.
 
-> groundNormalForm :: MonadSolve cs m m' => Nondet cs m a -> cs -> m' NormalForm
-> groundNormalForm  = evalStateT . gnf . untyped
+> groundNormalForm :: Update cs m m' => Nondet cs m a -> cs -> m' NormalForm
+> groundNormalForm = evalStateT . gnf . untyped
 >
-> partialNormalForm :: (MonadSolve cs m m', ChoiceStore cs)
+> partialNormalForm :: (Update cs m m', ChoiceStore cs)
 >                   => Nondet cs m a -> cs -> m' NormalForm
 > partialNormalForm = evalStateT . pnf . untyped
 
@@ -62,13 +62,13 @@
 representation. Partial normal forms may contain unbound logic
 variables while ground normal forms are data terms.
 
-> gnf :: MonadSolve cs m m' => Untyped cs m -> StateT cs m' NormalForm
+> gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm
 > gnf = nf (\_ _ -> Just ()) NormalForm mkVar
 >
 > mkVar :: ID -> a -> NormalForm
-> mkVar (ID us) _ = Var (uniqFromSupply us)
+> mkVar (ID us) _ = Var (supplyValue us)
 >
-> pnf :: (MonadSolve cs m m', ChoiceStore cs)
+> pnf :: (Update cs m m', ChoiceStore cs)
 >     => Untyped cs m -> StateT cs m' NormalForm
 > pnf x = nf lookupChoice ((return.).mkHNF) ((return.).FreeVar) x
 >     >>= nf lookupChoice NormalForm mkVar
@@ -81,17 +81,17 @@
 that `x` will be bound in the result when we encounter it for the
 first time.
 
-> nf :: MonadSolve cs m m'
->    => (Unique -> cs -> Maybe a)
+> nf :: Update cs m m'
+>    => (Int -> cs -> Maybe a)
 >    -> (Constr -> [nf] -> nf)
 >    -> (ID -> Untyped cs m -> nf)
 >    -> Untyped cs m -> StateT cs m' nf
 > nf lkp cns fv x = do
->   hnf <- solve x
+>   hnf <- updateState x
 >   case hnf of
 >     FreeVar u@(ID us) y ->
 >       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))
->             . lkp (uniqFromSupply us)
+>             . lkp (supplyValue us)
 >     Delayed _ resume -> get >>= nf lkp cns fv . resume
 >     Cons typ idx args -> do
 >       nfs <- mapM (nf lkp cns fv) args
@@ -100,7 +100,7 @@
 The `nf` function is used by all normal-form functions and performs
 all the work.
 
-> prim_eq :: MonadSolve cs m m
+> prim_eq :: Update cs m m
 >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool
 > prim_eq x y = do
 >   Cons _ ix xs <- solveCons x
@@ -117,10 +117,10 @@
 data that is used to define a typed equality test in the
 `Data.LazyNondet.Types.Bool` module.
 
-> solveCons :: MonadSolve cs m m
+> solveCons :: Update cs m m
 >           => Untyped cs m -> StateT cs m (HeadNormalForm cs m)
 > solveCons x = do
->   hnf <- solve x
+>   hnf <- updateState x
 >   case hnf of
 >     FreeVar _ y -> solveCons y
 >     Delayed _ res -> get >>= solveCons . res
diff --git a/src/Data/LazyNondet/Types.lhs b/src/Data/LazyNondet/Types.lhs
--- a/src/Data/LazyNondet/Types.lhs
+++ b/src/Data/LazyNondet/Types.lhs
@@ -19,14 +19,13 @@
 >
 > import Data.Data
 >
-> import Control.Monad.Constraint
+> import Control.Monad.Update
 >
-> import Unique
-> import UniqSupply
+> import Data.Supply
 >
-> newtype ID = ID UniqSupply
+> newtype ID = ID (Supply Int)
 >
-> data NormalForm = NormalForm Constr [NormalForm] | Var Unique
+> data NormalForm = NormalForm Constr [NormalForm] | Var Int
 
 The normal form of data is represented by the type `NormalForm` which
 defines a tree of constructors and logic variables. The type `Constr`
@@ -53,7 +52,7 @@
 data type that should be used for conversion into primitive data.
 
 > mkHNF :: Constr -> [Untyped cs m] -> HeadNormalForm cs m
-> mkHNF c args = Cons (constrType c) (constrIndex c) args
+> mkHNF c = Cons (constrType c) (constrIndex c)
 
 In head-normal forms we split the constructor representation into a
 representation of the data type and the index of the constructor, to
@@ -87,24 +86,24 @@
 
 > instance Show (HeadNormalForm cs [])
 >  where
->   show (FreeVar (ID u) _) = show (uniqFromSupply u)
+>   show (FreeVar (ID u) _) = '_':show (supplyValue u)
 >   show (Delayed _ _) = "<delayed>"
 >   show (Cons typ idx args) 
 >     | null args = show con
->     | otherwise = unwords (("("++show con):map show args++[")"])
+>     | otherwise = unwords (('(':show con):map show args++[")"])
 >    where con = indexConstr typ idx
 >
 > instance Show (Nondet cs [] a)
 >  where
 >   show = show . untyped
 >
-> instance Show (Nondet cs (ConstrT cs []) a)
+> instance Show (Nondet cs (UpdateT cs []) a)
 >  where
 >   show = show . untyped
 >
-> instance Show (HeadNormalForm cs (ConstrT cs []))
+> instance Show (HeadNormalForm cs (UpdateT cs []))
 >  where
->   show (FreeVar (ID u) _)  = show (uniqFromSupply u)
+>   show (FreeVar (ID u) _)  = '_':show (supplyValue u)
 >   show (Delayed _ _)         = "<delayed>"
 >   show (Cons typ idx [])   = show (indexConstr typ idx)
 >   show (Cons typ idx args) =
@@ -115,11 +114,12 @@
 
 > instance Show NormalForm
 >  where
->   showsPrec _ (Var u) = shows u
+>   showsPrec _ (Var u) = ('_':) . shows u
 >   showsPrec _ (NormalForm cons []) = shows cons
 >   showsPrec n x@(NormalForm cons args)
 >     | Just xs <- fromList x = shows xs
->     | n == 0    = shows cons . foldr1 (\y z -> (' ':).y.z) (map shows args)
+>     | n == 0 = shows cons . (' ':) . foldr1 (\y z -> y.(' ':).z)
+>                 (map (showsPrec 1) args)
 >     | otherwise = ('(':) . shows x . (')':)
 >
 > fromList :: NormalForm -> Maybe [NormalForm]
diff --git a/src/Data/LazyNondet/Types/Bool.lhs b/src/Data/LazyNondet/Types/Bool.lhs
--- a/src/Data/LazyNondet/Types/Bool.lhs
+++ b/src/Data/LazyNondet/Types/Bool.lhs
@@ -17,9 +17,10 @@
 > import Data.LazyNondet.Primitive
 >
 > import Control.Monad.State
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
+> import Control.Constraint.Choice
+>
 > instance ConsRep Bool where consRep = toConstr
 >
 > true :: Monad m => Nondet cs m Bool
@@ -43,11 +44,10 @@
 
 Some operations with `Bool`s:
 
-> not :: (MonadSolve cs m m, MonadConstr Choice m)
->     => Nondet cs m Bool -> cs -> Nondet cs m Bool
-> not x = caseOf_ x [pFalse (\_ -> true)] false
+> not :: Update cs m m => Nondet cs m Bool -> cs -> Nondet cs m Bool
+> not x = caseOf_ x [pFalse (const true)] false
 >
-> (===) :: MonadSolve cs m m
+> (===) :: Update cs m m
 >       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool
 > (x === y) cs = Typed $ do
 >   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs
diff --git a/src/Data/LazyNondet/Types/List.lhs b/src/Data/LazyNondet/Types/List.lhs
--- a/src/Data/LazyNondet/Types/List.lhs
+++ b/src/Data/LazyNondet/Types/List.lhs
@@ -15,9 +15,10 @@
 > import Data.LazyNondet
 > import Data.LazyNondet.Types.Bool
 >
-> import Control.Monad.Constraint
-> import Control.Monad.Constraint.Choice
+> import Control.Monad.Update
 >
+> import Control.Constraint.Choice
+>
 > instance ConsRep [()] where consRep = toConstr
 >
 > nil :: Monad m => Nondet cs m [a]
@@ -42,20 +43,17 @@
 
 > instance (ChoiceStore cs, Narrow cs a) => Narrow cs [a]
 >  where
->   narrow cs = withUnique $ \u1 u2 -> 
->                 oneOf [nil, unknown u1 ^: unknown u2] cs
+>   narrow cs u = withUnique (\u1 u2 -> 
+>                   (oneOf [nil, unknown u1 ^: unknown u2] cs u)) u
 
 Some operations on lists:
 
-> null :: (MonadSolve cs m m, MonadConstr Choice m)
->      => Nondet cs m [a] -> cs -> Nondet cs m Bool
-> null xs = caseOf_ xs [pNil (\_ -> true)] false
+> null :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m Bool
+> null xs = caseOf_ xs [pNil (const true)] false
 >
-> head :: (MonadSolve cs m m, MonadConstr Choice m)
->      => Nondet cs m [a] -> cs -> Nondet cs m a
+> head :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m a
 > head l = caseOf l [pCons (\_ x _ -> x)]
 >
-> tail :: (MonadSolve cs m m, MonadConstr Choice m)
->      => Nondet cs m [a] -> cs -> Nondet cs m [a]
+> tail :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m [a]
 > tail l = caseOf l [pCons (\_ _ xs -> xs)]
 
diff --git a/src/Data/LazyNondet/UniqueID.lhs b/src/Data/LazyNondet/UniqueID.lhs
--- a/src/Data/LazyNondet/UniqueID.lhs
+++ b/src/Data/LazyNondet/UniqueID.lhs
@@ -18,13 +18,13 @@
 >
 > import Control.Monad
 >
-> import UniqSupply
+> import Data.Supply
 
 Non-deterministic computations need a supply of unique identifiers in
 order to constrain shared choices.
 
 > initID :: IO ID
-> initID = liftM ID $ mkSplitUniqSupply 'x'
+> initID = liftM ID newNumSupply
 >
 > class With x a
 >  where
@@ -48,8 +48,7 @@
 >   type M ID (ID -> a) = M ID a
 >   type T ID (ID -> a) = T ID a
 >
->   with f (ID us) = withUnique (f (ID vs)) (ID ws)
->    where (vs,ws) = splitUniqSupply us
+>   with f (ID us) = with (f (ID (supplyLeft us))) (ID (supplyRight us))
 >
 > withUnique :: With ID a => a -> ID -> Nondet (C ID a) (M ID a) (T ID a)
 > withUnique = with