diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,5 +1,5 @@
 Name:			compdata
-Version:		0.5
+Version:		0.5.1
 Synopsis:            	Compositional Data Types
 Description:
 
@@ -129,7 +129,7 @@
   examples/Examples/Eval.hs
   examples/Examples/EvalM.hs
   examples/Examples/Desugar.hs
-  examples/Examples/Automata.hs,
+  examples/Examples/Automata/Compiler.hs,
   examples/Examples/Multi/Common.hs
   examples/Examples/Multi/Eval.hs
   examples/Examples/Multi/EvalI.hs
@@ -167,7 +167,7 @@
                         Data.Comp.Desugar,
                         Data.Comp.Automata,
                         Data.Comp.Automata.Product,
-                        Data.Comp.Zippable,
+                        Data.Comp.Number,
                         Data.Comp.Thunk,
 
                         Data.Comp.Multi,
diff --git a/examples/Examples/Automata.hs b/examples/Examples/Automata.hs
deleted file mode 100644
--- a/examples/Examples/Automata.hs
+++ /dev/null
@@ -1,147 +0,0 @@
-{-# LANGUAGE RankNTypes #-}
---------------------------------------------------------------------------------
--- |
--- Module      :  Examples.Automata
--- Copyright   :  (c) 2010-2011 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
--- This module defines tree automata based on compositional data types.
---
---------------------------------------------------------------------------------
-
-module Examples.Automata where
-
-import Data.Comp
-import Data.Maybe
-import Data.Traversable
-import Control.Monad
-
-
-{-| This type represents transition functions of deterministic
-bottom-up tree acceptors (DUTAs).  -}
-
-type DUTATrans f q = Alg f q
-
-{-| This data type represents deterministic bottom-up tree acceptors (DUTAs).
--}
-data DUTA f q = DUTA {
-      dutaTrans :: DUTATrans f q,
-      dutaAccept :: q -> Bool
-    }
-
-{-| This function runs the transition function of a DUTA on the given
-term. -}
-
-runDUTATrans :: Functor f => DUTATrans f q -> Term f -> q
-runDUTATrans = cata
-
-{-| This function checks whether a given DUTA accepts a term.  -}
-
-duta :: Functor f => DUTA f q -> Term f -> Bool
-duta DUTA{dutaTrans = trans, dutaAccept = accept} = accept . runDUTATrans trans
-
-
-
-{-| This type represents transition functions of non-deterministic
-bottom-up tree acceptors (NUTAs).  -}
-
-type NUTATrans f q = AlgM [] f q
-
-
-{-| This type represents non-deterministic bottom-up tree acceptors.
--}
-data NUTA f q = NUTA {
-      nutaTrans :: AlgM [] f q,
-      nutaAccept :: q -> Bool
-    }
-
-{-| This function runs the given transition function of a NUTA on the
-given term -}
-
-runNUTATrans :: Traversable f => NUTATrans f q -> Term f -> [q]
-runNUTATrans = cataM
-
-{-| This function checks whether a given NUTA accepts a term. -}
-
-nuta :: Traversable f => NUTA f q -> Term f -> Bool
-nuta NUTA{nutaTrans = trans, nutaAccept = accept} = any accept . runNUTATrans trans
-
-
-{-| This function determinises the given NUTA.  -}
-
-determNUTA :: (Traversable f) => NUTA f q -> DUTA f [q]
-determNUTA n = DUTA{
-               dutaTrans = algM $ nutaTrans n,
-               dutaAccept = any $ nutaAccept n}
-
-{-| This function represents transition functions of
-deterministic bottom-up tree transducers (DUTTs).  -}
-
-type DUTTTrans f g q = forall a. f (q,a) -> (q, Cxt Hole g a)
-
-{-| This function transforms a DUTT transition function into an
-algebra.  -}
-
-duttTransAlg :: (Functor f, Functor g)  => DUTTTrans f g q -> Alg f (q, Term g)
-duttTransAlg trans = fmap injectCxt . trans 
-
-{-| This function runs the given DUTT transition function on the given
-term.  -}
-
-runDUTTTrans :: (Functor f, Functor g)  => DUTTTrans f g q -> Term f -> (q, Term g)
-runDUTTTrans = cata . duttTransAlg
-
-{-| This data type represents deterministic bottom-up tree
-transducers. -}
-
-data DUTT f g q = DUTT {
-      duttTrans :: DUTTTrans f g q,
-      duttAccept :: q -> Bool
-    }
-
-{-| This function transforms the given term according to the given
-DUTT and returns the resulting term provided it is accepted by the
-DUTT. -}
-
-dutt :: (Functor f, Functor g) => DUTT f g q -> Term f -> Maybe (Term g)
-dutt DUTT{duttTrans = trans, duttAccept = accept} = accept' . runDUTTTrans trans
-    where accept' (q,res)
-              | accept q = Just res
-              | otherwise = Nothing
-
-{-| This type represents transition functions of non-deterministic
-bottom-up tree transducers (NUTTs).  -}
-
-type NUTTTrans f g q = forall a. f (q,a) -> [(q, Cxt Hole g a)]
-
-{-| This function transforms a NUTT transition function into a monadic
-algebra.  -}
-
-nuttTransAlg :: (Functor f, Functor g)  => NUTTTrans f g q -> AlgM [] f (q, Term g)
-nuttTransAlg trans = liftM (fmap injectCxt) . trans 
-
-{-| This function runs the given NUTT transition function on the given
-term.  -}
-
-runNUTTTrans :: (Traversable f, Functor g)  => NUTTTrans f g q -> Term f -> [(q, Term g)]
-runNUTTTrans = cataM . nuttTransAlg
-
-{-| This data type represents non-deterministic bottom-up tree
-transducers (NUTTs). -}
-
-data NUTT f g q = NUTT {
-      nuttTrans :: NUTTTrans f g q,
-      nuttAccept :: q -> Bool
-    }
-
-{-| This function transforms the given term according to the given
-NUTT and returns a list containing all accepted results. -}
-
-nutt :: (Traversable f, Functor g) => NUTT f g q -> Term f -> [Term g]
-nutt NUTT{nuttTrans = trans, nuttAccept = accept} = mapMaybe accept' . runNUTTTrans trans
-    where accept' (q,res)
-              | accept q = Just res
-              | otherwise = Nothing
diff --git a/examples/Examples/Automata/Compiler.hs b/examples/Examples/Automata/Compiler.hs
new file mode 100644
--- /dev/null
+++ b/examples/Examples/Automata/Compiler.hs
@@ -0,0 +1,192 @@
+{-# LANGUAGE TemplateHaskell, FlexibleContexts, MultiParamTypeClasses,
+TypeOperators, FlexibleInstances, UndecidableInstances,
+ScopedTypeVariables, TypeSynonymInstances, GeneralizedNewtypeDeriving,
+OverlappingInstances #-}
+
+module Examples.Automata.Compiler where
+
+import Data.Comp.Automata
+import Data.Comp.Derive
+import Data.Comp.Ops
+import Data.Comp hiding (height)
+import Data.Foldable
+import Prelude hiding (foldl)
+
+import Data.Set (Set, union, singleton, delete, member)
+import qualified Data.Set as Set
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+
+type Var = String
+
+data Val a = Const Int
+data Op a  = Plus a a
+           | Times a a
+type Core = Op :+: Val
+data Let a = Let Var a a
+           | Var Var
+
+type CoreLet = Let :+: Core
+
+data Sugar a = Neg a
+             | Minus a a
+
+$(derive [makeFunctor, makeFoldable, makeTraversable, smartConstructors, makeShowF]
+  [''Val, ''Op, ''Let, ''Sugar])
+
+
+class Eval f where
+    evalSt :: UpState f Int
+
+$(derive [liftSum] [''Eval])
+
+instance Eval Val where
+    evalSt (Const i) = i
+
+instance Eval Op where
+    evalSt (Plus x y) = x + y
+    evalSt (Times x y) = x * y
+
+type Addr = Int
+
+data Instr = Acc Int
+           | Load Addr
+           | Store Addr
+           | Add Int
+           | Sub Int
+           | Mul Int
+             deriving (Show)
+
+type Code = [Instr]
+
+data MState = MState {
+      mRam :: Map Addr Int,
+      mAcc :: Int }
+
+runCode :: Code -> MState -> MState
+runCode [] = id
+runCode (ins:c) = runCode c . step ins 
+    where step (Acc i) s = s{mAcc = i}
+          step (Load a) s = case Map.lookup a (mRam s) of
+              Nothing -> error $ "memory cell " ++ show a ++ " is not set"
+              Just n -> s {mAcc = n}
+          step (Store a) s = s {mRam = Map.insert a (mAcc s) (mRam s)}
+          step (Add a) s = exec (+) a s
+          step (Sub a) s = exec (-) a s
+          step (Mul a) s = exec (*) a s
+          exec op a s = case Map.lookup a (mRam s) of
+                        Nothing -> error $ "memory cell " ++ show a ++ " is not set"
+                        Just n -> s {mAcc = mAcc s `op` n}
+
+
+runCode' :: Code -> Int
+runCode' c = mAcc $ runCode c MState{mRam = Map.empty, mAcc = error "accumulator is not set"}
+
+
+-- | Defines the height of an expression.
+heightSt :: Foldable f => UpState f Int
+heightSt t = foldl max 0 t + 1
+
+tmpAddrSt :: Foldable f => UpState f Int
+tmpAddrSt = (+1) . heightSt
+
+
+newtype VarAddr = VarAddr {varAddr :: Int} deriving (Eq, Show, Num)
+
+class VarAddrSt f where
+  varAddrSt :: DownState f VarAddr
+  
+instance (VarAddrSt f, VarAddrSt g) => VarAddrSt (f :+: g) where
+    varAddrSt (q,Inl x) = varAddrSt (q, x)
+    varAddrSt (q,Inr x) = varAddrSt (q, x)
+
+instance VarAddrSt Let where
+  varAddrSt (d, Let _ _ x) = x `Map.singleton` (d + 2)
+  varAddrSt _ = Map.empty
+  
+instance VarAddrSt f where
+  varAddrSt _ = Map.empty
+
+
+type Bind = Map Var Int
+
+bindSt :: (Let :<: f,VarAddr :< q) => DDownState f q Bind
+bindSt t = case proj t of
+             Just (Let v _ e) -> Map.singleton e q'
+                       where q' = Map.insert v (varAddr above) above
+             _ -> Map.empty
+
+-- | Defines the code that an expression is compiled to. It depends on
+-- an integer state that denotes the height of the current node.
+class CodeSt f q where
+    codeSt :: DUpState f q Code
+
+instance (CodeSt f q, CodeSt g q) => CodeSt (f :+: g) q where
+    codeSt (Inl x) = codeSt x
+    codeSt (Inr x) = codeSt x
+  
+
+instance CodeSt Val q where
+    codeSt (Const i) = [Acc i]
+
+instance (Int :< q) => CodeSt Op q where
+    codeSt (Plus x y) = below x ++ [Store i] ++ below y ++ [Add i]
+        where i = below y
+    codeSt (Times x y) = below x ++ [Store i] ++ below y ++ [Mul i]
+        where i = below y
+
+instance (VarAddr :< q, Bind :< q) => CodeSt Let q where
+    codeSt (Let _ b e) = below b ++ [Store i] ++ below e
+                    where i = varAddr above
+    codeSt (Var v) = case Map.lookup v above of
+                       Nothing -> error $ "unbound variable " ++ v
+                       Just i -> [Load i]
+
+compile' :: (CodeSt f (Code,Int), Foldable f, Functor f) => Term f -> Code
+compile' = fst . runDUpState (codeSt `prodDUpState` dUpState tmpAddrSt)
+
+
+exComp' = compile' (iConst 2 `iPlus` iConst 3 :: Term Core)
+
+
+
+compile :: (CodeSt f ((Code,Int),(Bind,VarAddr)), Traversable f, Functor f, Let :<: f, VarAddrSt f)
+           => Term f -> Code
+compile = fst . runDState 
+          (codeSt `prodDUpState` dUpState tmpAddrSt)
+          (bindSt `prodDDownState` dDownState varAddrSt)
+          (Map.empty, VarAddr 1)
+          
+
+exComp = compile (iLet "x" (iLet "x" (iConst 5) (iConst 10 `iPlus` iVar "x")) (iConst 2 `iPlus` iVar "x") :: Term CoreLet)
+
+-- | Defines the set of free variables
+class VarsSt f where
+    varsSt :: UpState f (Set Var)
+
+$(derive [liftSum] [''VarsSt])
+
+instance VarsSt Val where
+    varsSt _ = Set.empty
+
+instance VarsSt Op where
+    varsSt (Plus x y) = x `union` y
+    varsSt (Times x y) = x `union` y
+
+instance VarsSt Let where
+    varsSt (Var v) = singleton v
+    varsSt (Let v x y) = (if v `member` y then x else Set.empty) `union` delete v y
+
+-- | Stateful homomorphism that removes unnecessary let bindings.
+remLetHom :: (Set Var :< q, Let :<: f, Functor f) => QHom f q f
+remLetHom t = case proj t of
+                Just (Let v _ y) 
+                    | not (v `member` below y) -> Hole y
+                _ -> simpCxt t
+
+-- | Removes unnecessary let bindings.
+remLet :: (Let :<: f, Functor f, VarsSt f) => Term f -> Term f
+remLet = runUpHom varsSt remLetHom
+
+exLet = remLet (iLet "x" (iConst 3) (iConst 2 `iPlus` iVar "y") :: Term CoreLet)
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -2,7 +2,7 @@
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Automata
--- Copyright   :  (c) 2010-2011 Patrick Bahr
+-- Copyright   :  (c) 2010-2012 Patrick Bahr
 -- License     :  BSD3
 -- Maintainer  :  Patrick Bahr <paba@diku.dk>
 -- Stability   :  experimental
@@ -11,14 +11,19 @@
 -- This module defines stateful term homomorphisms. This (slightly
 -- oxymoronic) notion extends per se stateless term homomorphisms with
 -- a state that is maintained separately by a bottom-up or top-down
--- tree automaton.
+-- state transformation. Additionally, this module also provides
+-- combinators to run state transformations themselves.
+-- 
+-- Like regular term homomorphisms also stateful homomorphisms (as
+-- well as transducers) can be lifted to annotated signatures
+-- (cf. Data.Comp.Annotation").
 --
 --------------------------------------------------------------------------------
 
 module Data.Comp.Automata
-    ( module Data.Comp.Automata.Product
+    (
     -- * Stateful Term Homomorphisms
-    , QHom
+      QHom
     , below
     , above
     -- ** Bottom-Up State Propagation
@@ -77,9 +82,11 @@
     , (&)
     , (|->)
     , o
+    -- * Product State Spaces
+    , module Data.Comp.Automata.Product
     ) where
 
-import Data.Comp.Zippable
+import Data.Comp.Number
 import Data.Comp.Automata.Product
 import Data.Comp.Term
 import Data.Comp.Algebra
@@ -87,6 +94,7 @@
 import qualified Data.Map as Map
 
 
+
 -- The following are operators to specify finite mappings.
 
 
@@ -117,13 +125,13 @@
 
 -- | Turns the explicit parameters @?above@ and @?below@ into explicit
 -- ones.
-explicit :: q -> (a -> q) -> ((?above :: q, ?below :: a -> q) => b) -> b
-explicit ab be x = x where ?above = ab; ?below = be
+explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b
+explicit x ab be = x where ?above = ab; ?below = be
 
 
 -- | This type represents stateful term homomorphisms. Stateful term
 -- homomorphisms have access to a state that is provided (separately)
--- by a DUTA or a DDTA (or both).
+-- by a bottom-up or top-down state transformation function (or both).
 type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
 
 -- -- | This type represents (pure, i.e. stateless) homomorphism by
@@ -143,7 +151,7 @@
 
 type UpTrans f q g = forall a. f (q,a) -> (q, Context g a)
 
--- | This function transforms DUTT transition function into an
+-- | This function transforms a DUTT transition function into an
 -- algebra.
 
 upAlg :: (Functor g)  => UpTrans f q g -> Alg f (q, Term g)
@@ -224,7 +232,7 @@
 upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g
 upTrans st f t = (q, c)
     where q = st $ fmap fst t
-          c = fmap snd $ explicit q fst f t
+          c = fmap snd $ explicit f q fst t
 
 -- | This function applies a given stateful term homomorphism with
 -- a state space propagated by the given DUTA to a term.
@@ -249,7 +257,7 @@
 -- | This combinator turns a GDUTA with the smallest possible state
 -- space into a DUTA.
 upState :: DUpState f q q -> UpState f q
-upState f s = res where res = explicit res id f s
+upState f s = res where res = explicit f res id s
 
 -- | This combinator runs a GDUTA on a term.
 runDUpState :: Functor f => DUpState f q q -> Term f -> q
@@ -341,23 +349,24 @@
           final (RState q) = (p, q)
           final (BState p q) = (p,q)
 
+
 -- | Apply the given state mapping to the given functorial value by
 -- adding the state to the corresponding index if it is in the map and
 -- otherwise adding the provided default state.
-appMap :: Zippable f => (forall i . Ord i => f i -> Map i q)
+appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
                        -> q -> f b -> f (q,b)
 appMap qmap q s = fmap qfun s'
     where s' = number s
           qfun k@(Numbered (_,a)) = (Map.findWithDefault q k (qmap s') ,a)
 
 -- | This function constructs a DDTT from a given stateful term-- homomorphism with the state propagated by the given DDTA.
-downTrans :: Zippable f => DownState f q -> QHom f q g -> DownTrans f q g
-downTrans st f (q, s) = explicit q fst f (appMap (curry st q) q s)
+downTrans :: Traversable f => DownState f q -> QHom f q g -> DownTrans f q g
+downTrans st f (q, s) = explicit f q fst (appMap (curry st q) q s)
 
 
 -- | This function applies a given stateful term homomorphism with a
 -- state space propagated by the given DDTA to a term.
-runDownHom :: (Zippable f, Functor g)
+runDownHom :: (Traversable f, Functor g)
             => DownState f q -> QHom f q g -> q -> Term f -> Term g
 runDownHom st h = runDownTrans (downTrans st h)
 
@@ -375,7 +384,7 @@
 -- space into a DDTA.
 downState :: DDownState f q q -> DownState f q
 downState f (q,s) = res
-    where res = explicit q bel f s
+    where res = explicit f q bel s
           bel k = Map.findWithDefault q k res
 
 
@@ -394,19 +403,19 @@
 -- | This combinator combines a bottom-up and a top-down state
 -- transformations. Both state transformations can depend mutually
 -- recursive on each other.
-runDState :: Zippable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u
+runDState :: Traversable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u
 runDState up down d (Term t) = u where
         t' = fmap bel $ number t
         bel (Numbered (i,s)) = 
             let d' = Map.findWithDefault d (Numbered (i,undefined)) m
             in Numbered (i, (runDState up down d' s, d'))
-        m = explicit (u,d) unNumbered down t'
-        u = explicit (u,d) unNumbered up t'
+        m = explicit down (u,d) unNumbered t'
+        u = explicit up (u,d) unNumbered t'
 
 -- | This combinator runs a stateful term homomorphisms with a state
 -- space produced both on a bottom-up and a top-down state
 -- transformation.
-runQHom :: (Zippable f, Functor g) =>
+runQHom :: (Traversable f, Functor g) =>
            DUpState f (u,d) u -> DDownState f (u,d) d -> 
            QHom f (u,d) g ->
            d -> Term f -> (u, Term g)
@@ -416,6 +425,6 @@
             let d' = Map.findWithDefault d (Numbered (i,undefined)) m
                 (u', s') = runQHom up down trans d' s
             in Numbered (i, ((u', d'),s'))
-        m = explicit (u,d) (fst . unNumbered) down t'
-        u = explicit (u,d) (fst . unNumbered) up t'
-        t'' = appCxt $ fmap (snd . unNumbered) $  explicit (u,d) (fst . unNumbered) trans t'
+        m = explicit down (u,d) (fst . unNumbered) t'
+        u = explicit up (u,d) (fst . unNumbered) t'
+        t'' = appCxt $ fmap (snd . unNumbered) $  explicit trans (u,d) (fst . unNumbered) t'
diff --git a/src/Data/Comp/Automata/Product.hs b/src/Data/Comp/Automata/Product.hs
--- a/src/Data/Comp/Automata/Product.hs
+++ b/src/Data/Comp/Automata/Product.hs
@@ -18,10 +18,8 @@
 
 instance a :< a where
     pr = id
-    up = const
 
 $(genAllInsts 7)
 
 instance (c :< b) => c :< (a,b) where
     pr = pr . snd
-    up z (x,y) = (x,up z y)
diff --git a/src/Data/Comp/Automata/Product/Derive.hs b/src/Data/Comp/Automata/Product/Derive.hs
--- a/src/Data/Comp/Automata/Product/Derive.hs
+++ b/src/Data/Comp/Automata/Product/Derive.hs
@@ -16,10 +16,9 @@
 import Language.Haskell.TH
 
 -- | An instance @a :< b@ means that @a@ is a component of @b@. @a@
--- can be extracted from @b@ via the method 'ex'.
+-- can be extracted from @b@ via the method 'pr'.
 class a :< b where
     pr :: b -> a
-    up :: a -> b -> b
 
 data Dir = L | R
          deriving Show
@@ -38,8 +37,7 @@
   n <- newName "a"
   ty <- genType n dir
   ex <- genEx dir
-  up <- genUp dir
-  return $ InstanceD [] (ConT (mkName ":<") `AppT` VarT n `AppT` ty) [ex,up]
+  return $ InstanceD [] (ConT (mkName ":<") `AppT` VarT n `AppT` ty) [ex]
 
 genType :: Name -> [Dir] -> Q Type
 genType n = gen
@@ -58,12 +56,6 @@
   n <- newName "x"
   p <- genPat n dir
   return $ FunD (mkName "pr") [Clause [p] (NormalB (VarE n)) []]
-
-genUp :: [Dir] -> DecQ
-genUp dir = do
-  n <- newName "x"
-  (p,e) <- genPatExp n dir
-  return $ FunD (mkName "up") [Clause [VarP n,p] (NormalB e) []]
 
 genPatExp :: Name -> [Dir] -> Q (Pat, Exp)
 genPatExp n = gen where
diff --git a/src/Data/Comp/Number.hs b/src/Data/Comp/Number.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Comp/Number.hs
@@ -0,0 +1,45 @@
+--------------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Comp.Number
+-- Copyright   :  (c) 2012 Patrick Bahr
+-- License     :  BSD3
+-- Maintainer  :  Patrick Bahr <paba@diku.dk>
+-- Stability   :  experimental
+-- Portability :  non-portable (GHC Extensions)
+-- 
+-- This module provides functionality to number the components of a
+-- functorial value with consecutive integers.
+--
+--------------------------------------------------------------------------------
+
+module Data.Comp.Number 
+    ( Numbered (..)
+    , unNumbered
+    , number
+    , Traversable ()) where
+
+import Data.Traversable
+
+import Control.Monad.State hiding (mapM)
+import Prelude hiding (mapM)
+
+
+-- | This type is used for numbering components of a functorial value.
+newtype Numbered a = Numbered (Int, a)
+
+unNumbered :: Numbered a -> a
+unNumbered (Numbered (_, x)) = x
+
+instance Eq (Numbered a) where
+    Numbered (i,_) == Numbered (j,_) = i == j
+
+instance Ord (Numbered a) where
+    compare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j
+
+-- | This function numbers the components of the given functorial
+-- value with consecutive integers starting at 0.
+number :: Traversable f => f a -> f (Numbered a)
+number x = fst $ runState (mapM run x) 0 where
+  run b = do n <- get
+             put (n+1)
+             return $ Numbered (n,b)
diff --git a/src/Data/Comp/Thunk.hs b/src/Data/Comp/Thunk.hs
--- a/src/Data/Comp/Thunk.hs
+++ b/src/Data/Comp/Thunk.hs
@@ -41,7 +41,7 @@
 import Data.Comp.Algebra
 import Data.Comp.Ops
 import Data.Comp.Sum
-import Data.Comp.Zippable
+import Data.Comp.Number
 import Data.Foldable hiding (and)
 
 import qualified Data.Set as Set
@@ -162,7 +162,7 @@
 -- of the arguments of a functor application strict. The first
 -- argument of this combinator specifies which positions are supposed
 -- to be strict.
-strictAt :: (f :<: g, Traversable f, Zippable f, Monad m) => Pos f ->  f (TermT m g) -> TermT m g
+strictAt :: (f :<: g, Traversable f, Monad m) => Pos f ->  f (TermT m g) -> TermT m g
 strictAt p s = thunk $ liftM inject $ mapM run s'
     where s'  = number s
           isStrict e = Set.member e $ Set.fromList $ p s'
diff --git a/src/Data/Comp/Zippable.hs b/src/Data/Comp/Zippable.hs
deleted file mode 100644
--- a/src/Data/Comp/Zippable.hs
+++ /dev/null
@@ -1,66 +0,0 @@
---------------------------------------------------------------------------------
--- |
--- Module      :  Data.Comp.Zippable
--- Copyright   :  (c) 2011 Patrick Bahr
--- License     :  BSD3
--- Maintainer  :  Patrick Bahr <paba@diku.dk>
--- Stability   :  experimental
--- Portability :  non-portable (GHC Extensions)
---
---
---------------------------------------------------------------------------------
-
-module Data.Comp.Zippable
-    ( Zippable (..)
-    , Numbered(..)
-    , unNumbered
-    , number
-    , number'
-    , Stream(..)
-    , (<:>)) where
-
--- import Data.Stream (Stream(..), (<:>))
-
-data Stream a = Cons a (Stream a) deriving (Eq, Ord)
-
-infixr 5 <:>
--- | The @ \<:\> @ operator is an infix version of the 'Cons'
--- constructor.
-(<:>) :: a -> Stream a -> Stream a
-(<:>) = Cons
-
--- | Instances of this class provide a generalisation of the zip
--- function on the list functor.
-class Functor f => Zippable f where
-    fzip :: Stream a -> f b -> f (a,b)
-    fzip = fzipWith (\ x y -> (x,y))
-    fzipWith :: (a -> b -> c) -> Stream a -> f b -> f c
-    fzipWith f s l = fmap (uncurry f) (fzip s l)
-
--- | This type is used for applying a DDTAs.
-newtype Numbered a = Numbered (Int, a)
-
-unNumbered :: Numbered a -> a
-unNumbered (Numbered (_, x)) = x
-
-instance Eq (Numbered a) where
-    Numbered (i,_) == Numbered (j,_) = i == j
-
-instance Ord (Numbered a) where
-    compare (Numbered (i,_))  (Numbered (j,_)) = i `compare` j
-
-
-number :: Zippable f => f a -> f (Numbered a)
-number t = fzipWith (curry Numbered) (nums 0) t
-    where nums x = x `Cons` nums (x+1)
-
-number' :: Zippable f => f a -> f (Int, a)
-number' t = fzipWith num (nums 0) t
-    where nums x = x <:> nums (x+1)
-          num n a = (n,a)
-
-instance Zippable [] where
-    fzip (Cons x xs) (y:ys) = (x,y) : fzip xs ys
-    fzip _ []  = []
-    fzipWith f (Cons x xs) (y:ys) = f x y : fzipWith f xs ys
-    fzipWith _ _ [] = []