diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       2009.1.23.2
+Version:       2009.1.24
 Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
diff --git a/src/CFLP.lhs b/src/CFLP.lhs
--- a/src/CFLP.lhs
+++ b/src/CFLP.lhs
@@ -28,7 +28,10 @@
 > import Control.Monad.State
 >
 > import CFLP.Data
+> import CFLP.Data.Types
+>
 > import CFLP.Control.Monad.Update
+>
 > import CFLP.Control.Strategy
 
 The type class `CFLP` amalgamates all class constraints on constraint
@@ -65,12 +68,12 @@
 
 > eval, evalPartial
 >   :: (Monad s, CFLP s, Generic a) => s (Ctx s) -> Computation a -> IO [a]
-> eval        s = liftM (liftM primitive) . evaluate s groundNormalForm
-> evalPartial s = liftM (liftM primitive) . evaluate s partialNormalForm
+> eval        s = liftM (liftM primitive) . evaluate s (groundNormalForm s)
+> evalPartial s = liftM (liftM primitive) . evaluate s (partialNormalForm s)
 >
 > evalPrint :: (Monad s, CFLP s, Generic a)
 >           => s (Ctx s) -> Computation a -> IO ()
-> evalPrint s op = evaluate s partialNormalForm op >>= printSols
+> evalPrint s op = evaluate s (partialNormalForm s) op >>= printSols
 >
 > printSols :: Show a => [a] -> IO ()
 > printSols []     = putStrLn "No more solutions."
@@ -89,10 +92,10 @@
 
 > evaluate :: CFLP s
 >          => s (Ctx s)
->          -> (Nondet (Ctx s) s a -> Context (Ctx s) -> Res s b)
+>          -> (Nondet (Ctx s) s a -> Res s b)
 >          -> Computation a
 >          -> IO [b]
 > evaluate s evalNondet op = do
 >   i <- initID
 >   return $ enumeration $
->     evalNondet (op (Context (emptyContext s)) i) $ Context (emptyContext s)
+>     evalNondet (Typed (s >>= untyped . flip op i . Context))
diff --git a/src/CFLP/Control/Strategy.lhs b/src/CFLP/Control/Strategy.lhs
--- a/src/CFLP/Control/Strategy.lhs
+++ b/src/CFLP/Control/Strategy.lhs
@@ -69,13 +69,6 @@
 
 Strategies provide the following operations:
 
->   emptyContext :: s c -> Ctx s
-
-yields an empty context of the associated type `Ctx s`. The argument
-of type `s c` is sometimes necessary to satisfy the type checker. It
-must always be safe to pass undefined, i.e., the argument must be
-ignored.
-
 >   choose :: c -> Int -> [s a] -> s a
 
 is used to cconstruct non-deterministic choices of computations. We
@@ -114,11 +107,6 @@
 
 The operation
 
->   emptyContext _ = ()
-
-yields `()` because stores are ignored by (untransformed) monadic
-strategies.
-
 >   choose _ _ [x] = x
 >   choose _ _ xs  = foldr mplus mzero xs
 
@@ -192,11 +180,6 @@
 that uses the base strategy. The first parameter is used to support
 type checking and must be ignored.
 
->   extendContext :: t s c -> Ctx s -> Ctx (t s)
-
-may extend the evaluation context of the base strategy. Again, the
-first argument must be ignored by instantiations of `StrategyT`.
-
 >   extendChoices :: (Monad s, MonadUpdate c s)
 >                 => c -> Int -> [t s a] -> [t s a]
 >   extendChoices _ _ = id
@@ -221,14 +204,6 @@
 >       => Strategy c (t s)
 >  where
 
-The operation `emptyContext` calls the corresponding operation of the
-base strategy and extends the result accoring to the transformer.
-
->   emptyContext c = extendContext c (emptyContext (undefined `forBaseOf` c))
-
-Here, we give a hint to the type checker using the type-constrained
-`const` function `forBaseOf` (defined below).
-
 The operation `choose` extends the choices according to the
 transformer and calls the `choose` operation of the base strategy with
 the resulting choices.
@@ -238,17 +213,10 @@
 >              . map (baseStrategy c)
 >              . extendChoices c n
 
-Finally, the predicate `isNarrowed` is altered according the strategy
+The predicate `isNarrowed` is altered according to the strategy
 transformer.
 
 >   isNarrowed c n = alterNarrowed c n (liftStrategy c (isNarrowed c n))
-
-The function `forBaseOf` is a `const` function with a specialised type
-that supports the type checker in finding the corresponding operation
-`emptyContext` for the base strategy.
-
-> forBaseOf :: s a -> t s a -> s a
-> forBaseOf = const
 
 
 Uniform Liftings
diff --git a/src/CFLP/Data/Primitive.lhs b/src/CFLP/Data/Primitive.lhs
--- a/src/CFLP/Data/Primitive.lhs
+++ b/src/CFLP/Data/Primitive.lhs
@@ -1,6 +1,10 @@
 % Primitive Generic Functions on Lazy Non-Deterministic Data
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
+> {-# LANGUAGE
+>       FlexibleContexts
+>   #-}
+>
 > module CFLP.Data.Primitive (
 >
 >   nondet, groundNormalForm, partialNormalForm,
@@ -29,7 +33,7 @@
 > nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
 > nf2hnf (Data label args) = Cons label (map (return . nf2hnf) args)
 > nf2hnf (Fun f) = Lambda (\x _ _ -> liftM (nf2hnf . f) $ gnf x)
->  where gnf x = groundNormalForm (Typed x) $
+>  where gnf x = flip groundNormalForm (Typed x) $ return $ 
 >                  error "Primitive.nf2hnf: primitive function uses context"
 
 The `...NormalForm` functions evaluate a non-deterministic value and
@@ -39,12 +43,19 @@
 variables while ground normal forms are data terms.
 
 > groundNormalForm :: (Monad s, Monad m, Update c s m)
->                  => Nondet c s a -> Context c -> m NormalForm
-> groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs
+>                  => s c -> Nondet c s a -> m NormalForm
+> groundNormalForm c x
+>   = evalStateT (updateState c) (undefined `asContextOf` c) >>=
+>     evalStateT (gnf (untyped x))
 >
 > partialNormalForm :: (Monad s, Strategy c s, Monad m, Update c s m)
->                   => Nondet c s a -> Context c -> m NormalForm
-> partialNormalForm x (Context cs) = evalStateT (pnf (untyped x)) cs
+>                   => s c -> Nondet c s a -> m NormalForm
+> partialNormalForm c x
+>   = evalStateT (updateState c) (undefined `asContextOf` c) >>=
+>     evalStateT (pnf (untyped x))
+>
+> asContextOf :: c -> s c -> c
+> asContextOf = const
 
 To compute ground normal forms, we ignore free variables and narrow
 them to ground terms. To compute partial normal forms, we do not
diff --git a/src/CFLP/Strategies.lhs b/src/CFLP/Strategies.lhs
--- a/src/CFLP/Strategies.lhs
+++ b/src/CFLP/Strategies.lhs
@@ -10,7 +10,7 @@
 >
 > module CFLP.Strategies (
 >
->   (<+), dfs, limDFS,
+>   dfs, limDFS,
 >
 >   module CFLP.Strategies.DepthFirst,
 >   module CFLP.Strategies.CallTimeChoice,
@@ -27,22 +27,15 @@
 > import CFLP.Strategies.DepthCounter
 > import CFLP.Strategies.DepthLimit
 
-We provide a combinator `(+>)` to transform a strategy with a strategy
-transformer (the type is not descriptive, so better ignore it..).
-
-> infixr 5 <+
->
-> (<+) :: (b -> c) -> (a -> b) -> d -> c
-> (t <+ s) _ = t (s undefined)
-
-For convenience, we provide shortcuts for useful strategies.
+We provide shortcuts for useful strategies.
 
-> dfs :: c -> CTC (Monadic (UpdateT (StoreCTC c) [])) a
-> dfs = callTimeChoice <+ dfsWithEvalTimeChoice
+> dfs :: CTC (Monadic (UpdateT (StoreCTC ()) [])) (StoreCTC ())
+> dfs = callTimeChoice dfsWithEvalTimeChoice
 >
-> limDFS :: c -> CTC (Depth (DepthLim (Monadic
->                     (UpdateT (StoreCTC (DepthCtx (DepthLimCtx c))) [])))) a
-> limDFS = callTimeChoice <+ countDepth <+ limitDepth <+ dfsWithEvalTimeChoice
+> limDFS :: Int -> CTC (Depth (DepthLim (Monadic
+>                       (UpdateT (StoreCTC (DepthCtx (DepthLimCtx ()))) []))))
+>                       (StoreCTC (DepthCtx (DepthLimCtx ())))
+> limDFS l = callTimeChoice.countDepth.limitDepth l$dfsWithEvalTimeChoice
 
 Finally, we provide instances for the type class `CFLP` that is a
 shortcut for the class constraints of CFLP computations.
diff --git a/src/CFLP/Strategies/CallTimeChoice.lhs b/src/CFLP/Strategies/CallTimeChoice.lhs
--- a/src/CFLP/Strategies/CallTimeChoice.lhs
+++ b/src/CFLP/Strategies/CallTimeChoice.lhs
@@ -126,12 +126,6 @@
 > type instance Ctx (CTC s) = StoreCTC (Ctx s)
 > type instance Res (CTC s) = CTC (Res s)
 
-We provide a constructor function that allows us to hide the
-corresponding newtype constructor.
-
-> callTimeChoice :: s a -> CTC s a
-> callTimeChoice = CTC
-
 The type `CTC` is a strategy transformer for strategies that have
 acces to a choice store.
 
@@ -140,9 +134,15 @@
 >   liftStrategy _ = CTC
 >   baseStrategy _ = fromCTC
 >
->   extendContext _ = StoreCTC noChoices
 >   extendChoices   = labeledChoices
 >
 >   alterNarrowed c n isn
 >     | isJust (lookupChoice n c) = return True
 >     | otherwise = isn
+
+We provide a strategy transformer function that is used to add
+call-time choice to arbitrary strategies.
+
+> callTimeChoice :: Monad s => s c -> CTC s (StoreCTC c)
+> callTimeChoice = CTC . liftM (StoreCTC noChoices)
+
diff --git a/src/CFLP/Strategies/DepthCounter.lhs b/src/CFLP/Strategies/DepthCounter.lhs
--- a/src/CFLP/Strategies/DepthCounter.lhs
+++ b/src/CFLP/Strategies/DepthCounter.lhs
@@ -1,4 +1,4 @@
-% Depth Monitoring for Non-Deterministic Computations.
+% Depth Monitoring for Non-Deterministic Computations
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
 This module provides a strategy transformer that extends the
@@ -70,11 +70,6 @@
 > type instance Ctx (Depth s) = DepthCtx (Ctx s)
 > type instance Res (Depth s) = Depth (Res s)
 
-The operation `countDepth` the `Depth` constructor.
-
-> countDepth :: s a -> Depth s a
-> countDepth = Depth
-
 The strategy-transformer instance increments the counter at each
 non-deterministic choice.
 
@@ -83,6 +78,9 @@
 >   liftStrategy _ = Depth
 >   baseStrategy _ = fromDepth
 >
->   extendContext _ = DepthCtx 0
->
 >   extendChoices c _ = map (update (return . incrementDepth c)>>)
+
+The operation `countDepth` adds a depth counter to a strategy.
+
+> countDepth :: Monad s => s c -> Depth s (DepthCtx c)
+> countDepth = Depth . liftM (DepthCtx 0)
diff --git a/src/CFLP/Strategies/DepthFirst.lhs b/src/CFLP/Strategies/DepthFirst.lhs
--- a/src/CFLP/Strategies/DepthFirst.lhs
+++ b/src/CFLP/Strategies/DepthFirst.lhs
@@ -26,6 +26,6 @@
 semantics. In order to get call-time choice, this needs to be
 transformed with the call-time choice transformer.
 
-> dfsWithEvalTimeChoice :: c -> Monadic (UpdateT c []) a
-> dfsWithEvalTimeChoice _ = Monadic undefined
+> dfsWithEvalTimeChoice :: Monadic (UpdateT c []) ()
+> dfsWithEvalTimeChoice = Monadic (return ())
 
diff --git a/src/CFLP/Strategies/DepthLimit.lhs b/src/CFLP/Strategies/DepthLimit.lhs
--- a/src/CFLP/Strategies/DepthLimit.lhs
+++ b/src/CFLP/Strategies/DepthLimit.lhs
@@ -1,4 +1,4 @@
-% Depth Limiting for Non-Deterministic Computations.
+% Depth Limiting for Non-Deterministic Computations
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
 This module provides a strategy transformer that extends the
@@ -43,12 +43,9 @@
 >
 >   resetDepthLimit _ l c = replace c (resetDepthLimit undefined l (project c))
 
-The default limit is 100, but you can use the operation
-`setDepthLimit` in computations to change it.
+The operation `setDepthLimit` is used in computations to change the
+depth limit.
 
-> defaultLimit :: Int
-> defaultLimit = 100
->
 > setDepthLimit :: (Monad s, DepthLimiter c, MonadUpdate c s)
 >               => c -> Int -> s ()
 > setDepthLimit c l = update (return . resetDepthLimit c l)
@@ -80,11 +77,6 @@
 > type instance Ctx (DepthLim s) = DepthLimCtx (Ctx s)
 > type instance Res (DepthLim s) = DepthLim (Res s)
 
-The operation `depthCounter` the `Depth` constructor.
-
-> limitDepth :: s a -> DepthLim s a
-> limitDepth = DepthLim
-
 The strategy-transformer instance increments the counter at each
 non-deterministic choice and prunes the choices if the limit is
 exceeded.
@@ -94,9 +86,13 @@
 >   liftStrategy _ = DepthLim
 >   baseStrategy _ = fromDepthLim
 >
->   extendContext _ = DepthLimCtx defaultLimit
->
 >   extendChoices c _ xs
 >     | currentDepth c < depthLimit c
 >       = map (update (return . incrementDepth c)>>) xs
 >     | otherwise = []
+
+The operation `limitDepth` adds a depth limit to a strategy.
+
+> limitDepth :: Monad s => Int -> s c -> DepthLim s (DepthLimCtx c)
+> limitDepth l = DepthLim . liftM (DepthLimCtx l)
+
diff --git a/src/CFLP/Tests.lhs b/src/CFLP/Tests.lhs
--- a/src/CFLP/Tests.lhs
+++ b/src/CFLP/Tests.lhs
@@ -26,7 +26,7 @@
 > assertResultsLimit :: (Generic a, Show a, Eq a)
 >                    => Maybe Int -> Computation a -> [a] -> Assertion
 > assertResultsLimit limit op expected = do
->   actual <- eval (limDFS ()) op
+>   actual <- eval (limDFS 100) op
 >   maybe id take limit actual @?= expected
 
 We provide auxiliary assertions `assertResults...` that compute (a
diff --git a/src/CFLP/Tests/HigherOrder.lhs b/src/CFLP/Tests/HigherOrder.lhs
--- a/src/CFLP/Tests/HigherOrder.lhs
+++ b/src/CFLP/Tests/HigherOrder.lhs
@@ -23,7 +23,7 @@
 >   , "apply non-deterministic choice" ~: applyChoice
 >   , "call-time choice" ~: callTimeChoice
 >   , "map shared unknowns" ~: mapSharedUnknowns
->   , "memeber with fold" ~: memberWithFold
+>   , "member with fold" ~: memberWithFold
 >   , "overApplication" ~: overApplication
 >   , "reverse with foldr" ~: reverseWithFoldr
 >   , "pointfree reverse" ~: pointfreeReverse