diff --git a/NanoProlog.cabal b/NanoProlog.cabal
--- a/NanoProlog.cabal
+++ b/NanoProlog.cabal
@@ -1,5 +1,5 @@
 Name:                NanoProlog
-Version:             0.2
+Version:             0.2.1
 Synopsis:            Very small  interpreter for a Prolog-like language
 Description:         This package was developed to demonstrate the ideas behind
                      the Prolog language. It contains a very small interpreter
@@ -10,7 +10,7 @@
 License:             BSD3
 license-file:        LICENSE
 Author:              Doaitse Swierstra, Jurriën Stutterheim
-Maintainer:          j.stutterheim@uu.nl
+Maintainer:          Jurriën Stutterheim <j.stutterheim@uu.nl>
 Stability:           Experimental
 Category:            Language
 Build-type:          Simple
diff --git a/src/Language/Prolog/NanoProlog/Interpreter.hs b/src/Language/Prolog/NanoProlog/Interpreter.hs
--- a/src/Language/Prolog/NanoProlog/Interpreter.hs
+++ b/src/Language/Prolog/NanoProlog/Interpreter.hs
@@ -44,8 +44,7 @@
 printSolutions ::  Result -> IO ()
 printSolutions result = sequence_
   [  do  sequence_  [  putStrLn (prefix ++ " " ++ show (subst env pr))
-                    |  (prefix, pr@(p :<-: pp)) <- reverse proof
---                  ,  length pp >0
+                    |  (prefix, pr) <- reverse proof
                     ]
          putStr "substitution: "
          putStrLn (show' env)
diff --git a/src/Language/Prolog/NanoProlog/NanoProlog.hs b/src/Language/Prolog/NanoProlog/NanoProlog.hs
--- a/src/Language/Prolog/NanoProlog/NanoProlog.hs
+++ b/src/Language/Prolog/NanoProlog/NanoProlog.hs
@@ -4,7 +4,8 @@
 {-# LANGUAGE FlexibleInstances #-}
 
 module Language.Prolog.NanoProlog.NanoProlog (
-     LowerCase
+     Env
+  ,  LowerCase
   ,  Result(..)
   ,  Rule((:<-:))
   ,  Subst(..)
@@ -12,6 +13,7 @@
   ,  Term(..)
   ,  emptyEnv
   ,  enumerateDepthFirst
+  ,  matches
   ,  pFun
   ,  pRule
   ,  pTerm
@@ -81,7 +83,15 @@
 instance Subst Rule where
   subst env (c :<-: cs) = subst env c :<-: subst env cs
 
-unify :: (Term, Term) -> Maybe Env-> Maybe Env
+matches :: (Term, Term) -> Maybe Env -> Maybe Env
+matches _       Nothing        = Nothing
+matches (t, u)  env@(Just m)   = match(subst m t) u
+  where  match  (Var x)     y  = Just (M.insert x y m)
+         match  (Fun x xs)  (Fun y ys)
+           |  x == y && length xs == length ys = foldr matches env (zip xs ys)
+         match  _           _  = Nothing
+
+unify :: (Term, Term) -> Maybe Env -> Maybe Env
 unify _       Nothing       = Nothing
 unify (t, u)  env@(Just m)  = uni (subst m t) (subst m u)
   where  uni  (Var x)  y        = Just (M.insert x  y  m)
@@ -94,9 +104,9 @@
 solve _      Nothing   _        = ApplyRules []
 solve _      (Just e)    []     = Done e
 solve rules  e  ((tg,t):ts)  = ApplyRules
-  [  (tg, rule, solve rules nextenv (zip (map (\ n -> tg ++ "." ++ show n) [1..]) cs ++ ts))
+  [  let  cts = map ((tg ++) . ('.' :) . show) ([1..] :: [Int]) `zip` cs ++ ts
+     in   (tg, rule, solve rules (unify (t, c) e) cts)
   |  rule@(c :<-: cs)  <- tag tg rules
-  ,  nextenv@(Just _)  <- [unify (t, c) e]
   ]
 
 -- ** Printing the solutions | `enumerateBreadthFirst` performs a
@@ -105,27 +115,27 @@
 -- root to the current node. At a successful leaf this contains the
 -- full proof.
 enumerateDepthFirst :: Proofs -> Result -> [(Proofs, Env)]
-enumerateDepthFirst proofs  (Done env) = [(proofs, env)]
-enumerateDepthFirst proofs  (ApplyRules bs) =
-  [ s  |  (tag, rule@(c :<-: cs), subTree) <- bs
-       ,  s <- enumerateDepthFirst ((tag, rule):proofs) subTree
+enumerateDepthFirst proofs (Done env)       = [(proofs, env)]
+enumerateDepthFirst proofs (ApplyRules bs)  =
+  [ s  |  (tag', rule, subTree) <- bs
+       ,  s <- enumerateDepthFirst ((tag', rule):proofs) subTree
   ]
 
 {-
 -- | `enumerateBreadthFirst` is still undefined, and is left as an
 -- exercise to the JCU students
-enumerateBreadthFirst :: Proofs -> [String] -> Result -> [(Proofs, Env)]
+enumerateBreadthFirst :: Proofs -> Result -> [(Proofs, Env)]
 -}
 
 -- | `printEnv` prints a single solution, showing only the variables
 -- that were introduced in the original goal
 show' :: Env -> String
 show' env = intercalate ", " . filter (not.null) . map showBdg $ M.assocs env
-  where  showBdg (x, t)  | isGlobVar x =  x ++ " <- " ++ showTerm t
-                         | otherwise = ""
-         showTerm t@(Var _)  = showTerm (subst env t)
-         showTerm (Fun f []) = f
-         showTerm (Fun f ts) = f ++ "(" ++ intercalate ", " (map showTerm ts) ++ ")"
+  where  showBdg (x, t)  | isGlobVar x  = x ++ " <- " ++ showTerm t
+                         | otherwise    = ""
+         showTerm t@(Var _)   = showTerm (subst env t)
+         showTerm (Fun f [])  = f
+         showTerm (Fun f ts)  = f ++ "(" ++ intercalate ", " (map showTerm ts) ++ ")"
          isGlobVar x = head x `elem` ['A'..'Z'] && last x `notElem` ['0'..'9']
 
 instance Show Term where
@@ -141,14 +151,17 @@
 showCommas l = intercalate ", " (map show l)
 
 -- ** Parsing Rules and Terms
-startParse :: (ListLike s b, Show b)  => P (Str b s LineColPos) a -> s
-                                      -> (a, [Error LineColPos])
+startParse :: (ListLike s b, Show b)  =>  P (Str b s LineColPos) a -> s
+                                      ->  (a, [Error LineColPos])
 startParse p inp  =  parse ((,) <$> p <*> pEnd)
                   $  createStr (LineColPos 0 0 0) inp
 
+pSepDot :: Parser String -> Parser [String]
+pSepDot p = (:) <$> p <*> pFoldr list_alg ((:) <$> pDot <*> p)
+
 pTerm, pVar, pFun :: Parser Term
 pTerm  = pVar  <|>  pFun
-pVar   = Var   <$>  lexeme (pList1 pUpper)
+pVar   = Var   <$>  lexeme ((++) <$> pList1 pUpper <*> (concat <$> pSepDot (pList1 pDigit) <|> pure []))
 pFun   = Fun   <$>  pLowerCase <*> (pParens pTerms `opt` [])
   where  pLowerCase :: Parser String
          pLowerCase = (:) <$> pLower <*> lexeme (pList (pLetter <|> pDigit))