diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2009-2012, Nick Smallbone
+Copyright (c) 2009-2014, Nick Smallbone
 
 All rights reserved.
 
diff --git a/quickspec.cabal b/quickspec.cabal
--- a/quickspec.cabal
+++ b/quickspec.cabal
@@ -1,5 +1,5 @@
 Name:                quickspec
-Version:             0.9.2
+Version:             0.9.3
 Cabal-version:       >=1.6
 Build-type:          Simple
 
@@ -90,5 +90,5 @@
     Test.QuickSpec.Utils.MemoValuation
 
   Build-depends:
-    base < 5, containers, transformers, QuickCheck,
+    base < 5, containers, transformers, QuickCheck >= 2.7,
     random, spoon >= 0.2, array, ghc-prim, mtl
diff --git a/src/Test/QuickSpec.hs b/src/Test/QuickSpec.hs
--- a/src/Test/QuickSpec.hs
+++ b/src/Test/QuickSpec.hs
@@ -33,14 +33,14 @@
    -- If you want to get equations over a type that isn't in `Ord`,
    -- you must use the `observerN` family of functions (below)
    -- to define an observation function for that type.
-   con, fun0, fun1, fun2, fun3, fun4,
+   con, fun0, fun1, fun2, fun3, fun4, fun5,
    -- * Adding functions whose results are not in `Ord`
    --
    -- | These functions work the same as `funN` (above),
    --   but don't use `Ord` to compare the results of the functions.
    --   Instead you can use the `observerN` family of functions (below)
    --   to define an observation function.
-   blind0, blind1, blind2, blind3, blind4,
+   blind0, blind1, blind2, blind3, blind4, blind5,
    -- * Adding variables to a signature
    vars,
    gvars,
diff --git a/src/Test/QuickSpec/Approximate.hs b/src/Test/QuickSpec/Approximate.hs
--- a/src/Test/QuickSpec/Approximate.hs
+++ b/src/Test/QuickSpec/Approximate.hs
@@ -4,6 +4,7 @@
 
 import Test.QuickCheck
 import Test.QuickCheck.Gen
+import Test.QuickCheck.Random
 import Test.QuickSpec.Signature
 import Test.QuickSpec.Term
 import Test.QuickSpec.Utils
@@ -36,7 +37,7 @@
   unlifted [] = return []
   unlifted (x:xs) = liftM2 (:) (lifted x) (lifted xs)
 
-approximate :: Partial a => (forall a. Partial a => a -> Maybe a) -> StdGen -> Int -> a -> a
+approximate :: Partial a => (forall a. Partial a => a -> Maybe a) -> QCGen -> Int -> a -> a
 approximate eval g n x = unGen (runReaderT (lifted x) (Plug plug)) g n
   where
     plug :: forall a. Partial a => Gen a -> Gen a
diff --git a/src/Test/QuickSpec/Generate.hs b/src/Test/QuickSpec/Generate.hs
--- a/src/Test/QuickSpec/Generate.hs
+++ b/src/Test/QuickSpec/Generate.hs
@@ -16,36 +16,40 @@
 import Text.Printf
 import Test.QuickSpec.Utils.Typeable
 import Test.QuickSpec.Utils
-import Test.QuickCheck.Gen
+import Test.QuickCheck.Gen hiding (generate)
+import Test.QuickCheck.Random
 import System.Random
 import Control.Spoon
 import Test.QuickSpec.Utils.MemoValuation
 
 terms :: Sig -> TypeRel Expr -> TypeRel Expr
-terms sig base =
+terms = termsSatisfying (const True)
+
+termsSatisfying :: (Term -> Bool) -> Sig -> TypeRel Expr -> TypeRel Expr
+termsSatisfying p sig base =
   TypeMap.fromList
-    [ Some (O (terms' sig base w))
+    [ Some (O (terms' p sig base w))
     | Some (Witness w) <- usort (saturatedTypes sig ++ variableTypes sig) ]
 
-terms' :: Typeable a => Sig -> TypeRel Expr -> a -> [Expr a]
-terms' sig base w =
-  filter (\t -> size 1 (term t) <= maxSize sig) $
+terms' :: Typeable a => (Term -> Bool) -> Sig -> TypeRel Expr -> a -> [Expr a]
+terms' p sig base w =
+  filter (\t -> size 1 (term t) <= maxSize sig && p (term t)) $
   map var (TypeRel.lookup w (variables sig)) ++
   map con (TypeRel.lookup w (constants sig)) ++
   [ app f x
   | Some (Witness w') <- lhsWitnesses sig w,
     x <- TypeRel.lookup w' base,
     not (isUndefined (term x)),
-    f <- terms' sig base (const w),
+    f <- terms' p sig base (const w),
     arity f > 0,
     not (isUndefined (term f)) ]
 
-test :: [(Valuation, StdGen, Int)] -> Sig ->
+test :: [(Valuation, QCGen, Int)] -> Sig ->
         TypeMap (List `O` Expr) -> TypeMap (TestResults `O` Expr)
 test vals sig ts = fmap (mapSome2 (test' vals sig)) ts
 
 test' :: forall a. Typeable a =>
-         [(Valuation, StdGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
+         [(Valuation, QCGen, Int)] -> Sig -> [Expr a] -> TestResults (Expr a)
 test' vals sig ts
   | not (testable sig (undefined :: a)) = discrete ts
   | otherwise =
@@ -58,33 +62,39 @@
     base = minTests sig `div` 2
     increment = minTests sig - base
 
-genSeeds :: Int -> IO [(StdGen, Int)]
+genSeeds :: Int -> IO [(QCGen, Int)]
 genSeeds maxSize = do
-  rnd <- newStdGen
+  rnd <- newQCGen
   let rnds rnd = rnd1 : rnds rnd2 where (rnd1, rnd2) = split rnd
   return (zip (rnds rnd) (concat (repeat [0,2..maxSize])))
 
-toValuation :: Strategy -> Sig -> (StdGen, Int) -> (Valuation, StdGen, Int)
+toValuation :: Strategy -> Sig -> (QCGen, Int) -> (Valuation, QCGen, Int)
 toValuation strat sig (g, n) =
   let (g1, g2) = split g
   in (memoValuation sig (unGen (valuation strat) g1 n), g2, n)
 
-generate :: Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr))
-generate strat sig | maxDepth sig < 0 =
+generate :: Bool -> Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr))
+generate shutUp strat sig = generateTermsSatisfying shutUp (const True) strat sig
+
+generateTermsSatisfying :: Bool -> (Term -> Bool) -> Strategy -> Sig -> IO (TypeMap (TestResults `O` Expr))
+generateTermsSatisfying shutUp p strat sig | maxDepth sig < 0 =
   ERROR "generate: maxDepth must be positive"
-generate strat sig | maxDepth sig == 0 = return TypeMap.empty
-generate strat sig = unbuffered $ do
+generateTermsSatisfying shutUp p strat sig | maxDepth sig == 0 = return TypeMap.empty
+generateTermsSatisfying shutUp p strat sig = unbuffered $ do
   let d = maxDepth sig
-  rs <- fmap (TypeMap.mapValues2 reps) (generate (const partialGen) (updateDepth (d-1) sig))
-  printf "Depth %d: " d
+      quietly x | shutUp = return ()
+                | otherwise = x
+  rs <- fmap (TypeMap.mapValues2 reps) (generate shutUp (const partialGen) (updateDepth (d-1) sig))
+  quietly $ printf "Depth %d: " d
   let count :: ([a] -> a) -> (forall b. f (g b) -> a) ->
                TypeMap (f `O` g) -> a
       count op f = op . map (some2 f) . TypeMap.toList
-      ts = terms sig rs
-  printf "%d terms, " (count sum length ts)
+      ts = termsSatisfying p sig rs
+  quietly $ printf "%d terms, " (count sum length ts)
   seeds <- genSeeds (maxQuickCheckSize sig)
   let cs = test (map (toValuation strat sig) seeds) sig ts
-  printf "%d tests, %d evaluations, %d classes, %d raw equations.\n"
+  quietly $
+    printf "%d tests, %d evaluations, %d classes, %d raw equations.\n"
       (count (maximum . (0:)) numTests cs)
       (count sum numResults cs)
       (count sum (length . classes) cs)
diff --git a/src/Test/QuickSpec/Main.hs b/src/Test/QuickSpec/Main.hs
--- a/src/Test/QuickSpec/Main.hs
+++ b/src/Test/QuickSpec/Main.hs
@@ -102,21 +102,26 @@
 quickSpec :: Signature a => a -> IO ()
 quickSpec = runTool $ \sig -> do
   putStrLn "== Testing =="
-  r <- generate (const partialGen) sig
+  r <- generate False (const partialGen) sig
   let clss = concatMap (some2 (map (Some . O) . classes)) (TypeMap.toList r)
+      univ = concatMap (some2 (map (tagged term))) clss
       reps = map (some2 (tagged term . head)) clss
       eqs = equations clss
   printf "%d raw equations; %d terms in universe.\n\n"
     (length eqs)
     (length reps)
 
-  let ctx = initial (maxDepth sig) (symbols sig) reps
+  let ctx = initial (maxDepth sig) (symbols sig) univ
       allEqs = map (some eraseEquation) eqs
       isBackground = all silent . eqnFuns
+      keep eq = not (isBackground eq) || absurd eq
+      absurd (t :=: u) = absurd1 t u || absurd1 u t
+      absurd1 (Var x) t = x `notElem` vars t
+      absurd1 _ _ = False
       (background, foreground) =
         partition isBackground allEqs
-      pruned = filter (not . isBackground)
-                 (prune ctx (map erase reps) id
+      pruned = filter keep
+                 (prune ctx (filter (not . isUndefined) (map erase reps)) id
                    (background ++ foreground))
       eqnFuns (t :=: u) = funs t ++ funs u
       isGround (t :=: u) = null (vars t) && null (vars u)
@@ -146,7 +151,7 @@
 sampleTerms :: Signature a => a -> IO ()
 sampleTerms = runTool $ \sig -> do
   putStrLn "== Testing =="
-  r <- generate (const partialGen) (updateDepth (maxDepth sig - 1) sig)
+  r <- generate False (const partialGen) (updateDepth (maxDepth sig - 1) sig)
   let univ = sort . concatMap (some2 (map term)) . TypeMap.toList . terms sig .
              TypeMap.mapValues2 reps $ r
   printf "Universe contains %d terms.\n\n" (length univ)
diff --git a/src/Test/QuickSpec/Prelude.hs b/src/Test/QuickSpec/Prelude.hs
--- a/src/Test/QuickSpec/Prelude.hs
+++ b/src/Test/QuickSpec/Prelude.hs
@@ -12,14 +12,14 @@
 -- | Just a type.
 --   You can instantiate your polymorphic functions at this type
 --   to include them in a signature.
-newtype A = A Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial)
-newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial)
-newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial)
+newtype A = A Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial, Show)
+newtype B = B Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial, Show)
+newtype C = C Int deriving (Eq, Ord, Typeable, Arbitrary, CoArbitrary, Partial, Show)
 
 -- | A type with two elements.
 --   Use this instead of @A@ if testing doesn't work well because
 --   the domain of @A@ is too large.
-data Two = One | Two deriving (Eq, Ord, Typeable)
+data Two = One | Two deriving (Eq, Ord, Typeable, Show)
 
 instance Arbitrary Two where
   arbitrary = elements [One, Two]
diff --git a/src/Test/QuickSpec/Signature.hs b/src/Test/QuickSpec/Signature.hs
--- a/src/Test/QuickSpec/Signature.hs
+++ b/src/Test/QuickSpec/Signature.hs
@@ -324,6 +324,12 @@
                  `mappend` typeSig (undefined :: d)
                  `mappend` typeSig (undefined :: e)
 
+primCon5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) =>
+          Int -> String -> (a -> b -> c -> d -> e -> f) -> Sig
+primCon5 n x f = primCon4 n x f
+                 `mappend` typeSig (undefined :: e)
+                 `mappend` typeSig (undefined :: f)
+
 -- | A constant.
 blind0 :: forall a. Typeable a => String -> a -> Sig
 blind0 = primCon0 0
@@ -343,6 +349,10 @@
 blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) =>
           String -> (a -> b -> c -> d -> e) -> Sig
 blind4 = primCon4 4
+-- | A function of arity 5.
+blind5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) =>
+          String -> (a -> b -> c -> d -> e -> f) -> Sig
+blind5 = primCon5 5
 
 ord :: (Ord a, Typeable a) => a -> Sig
 ord x = ordSig (Observer (pgen (return id)) `observing` x)
@@ -441,6 +451,13 @@
 fun4 x f = blind4 x f
            `mappend` ord (f undefined undefined undefined undefined)
 
+-- | A function of five arguments.
+fun5 :: (Typeable a, Typeable b, Typeable c, Typeable d,
+         Typeable e, Typeable f, Ord f) =>
+        String -> (a -> b -> c -> d -> e -> f) -> Sig
+fun5 x f = blind5 x f
+           `mappend` ord (f undefined undefined undefined undefined undefined)
+
 -- | An observation function of arity 1.
 observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig
 observer1 f = observerSig (Observer (pgen (return f)))
@@ -551,13 +568,15 @@
       where next = head (filter (`notElem` used) candidates)
             candidates
               | null wellTypedNames = ERROR "null allVars"
-              | otherwise = wellTypedNames ++ concat [ map (++ show i) wellTypedNames | i <- [1.. ] ]
+              | otherwise = concat [ map (++ suffix) wellTypedNames | suffix <- suffixes ]
             allVars =
               map (some (sym . unVariable))
                 (TypeRel.toList (variables sig)) ++
               ss
             wellTypedNames =
               [ name v | v <- allVars, symbolType v == symbolType x ]
+            suffixes =
+              concat ([sequence (replicate n ['a'..'z']) | n <- [0..]])
 
 constantSymbols, variableSymbols, symbols :: Sig -> [Symbol]
 constantSymbols sig =
diff --git a/src/Test/QuickSpec/Term.hs b/src/Test/QuickSpec/Term.hs
--- a/src/Test/QuickSpec/Term.hs
+++ b/src/Test/QuickSpec/Term.hs
@@ -7,9 +7,11 @@
 import Test.QuickSpec.Utils.Typeable
 import Test.QuickCheck
 import Test.QuickCheck.Gen
+import Test.QuickCheck.Gen.Unsafe
 import Data.Function
 import Data.Ord
 import Data.Char
+import Data.List
 import Test.QuickSpec.Utils
 
 data Symbol = Symbol {
@@ -51,7 +53,7 @@
       body (App f x) = Right (f, x)
 
 instance Show Term where
-  showsPrec p t = showString (showTerm p t)
+  showsPrec p t = showString (showTerm p (hideImplicit t))
    where
      brack s = "(" ++ s ++ ")"
      parenFun p s | p < 2 = s
@@ -69,6 +71,14 @@
      showTerm p (f `App` x) =
        parenFun p (showTerm 1 f ++ " " ++ showTerm 2 x)
 
+     hideImplicit (f `App` x)
+       | isImplicit x = f
+       | otherwise = hideImplicit f `App` hideImplicit x
+     hideImplicit t = t
+
+     isImplicit (Var v) | "_" `isPrefixOf` name v = True
+     isImplicit _ = False
+
 showOp :: String -> String
 showOp op | isOp op = "(" ++ op ++ ")"
           | otherwise = op
@@ -131,6 +141,11 @@
 mapVars f (Const x) = Const x
 mapVars f (App t u) = App (mapVars f t) (mapVars f u)
 
+mapConsts :: (Symbol -> Symbol) -> Term -> Term
+mapConsts f (Var x) = Var x
+mapConsts f (Const x) = Const (f x)
+mapConsts f (App t u) = App (mapConsts f t) (mapConsts f u)
+
 data Expr a = Expr {
   term :: Term,
   arity :: {-# UNPACK #-} !Int,
@@ -175,14 +190,13 @@
 -- Generate a random variable valuation
 newtype Valuation = Valuation { unValuation :: forall a. Variable a -> a }
 
-promoteVal :: (forall a. Gen (Variable a -> a)) -> Gen Valuation
-promoteVal g = MkGen (\r n -> Valuation (unGen g r n))
+promoteVal :: (forall a. Variable a -> Gen a) -> Gen Valuation
+promoteVal g = do
+  Capture eval <- capture
+  return (Valuation (eval . g))
 
 valuation :: Strategy -> Gen Valuation
-valuation strat = promoteVal (promote (\(Variable x) -> index (sym x) `variant'` strat (sym x) (value x)))
-  where -- work around the fact that split doesn't work
-        variant' 0 = variant (0 :: Int)
-        variant' n = variant (-1 :: Int) . variant' (n-1)
+valuation strat = promoteVal (\(Variable x) -> index (sym x) `variant` strat (sym x) (value x))
 
 var :: Variable a -> Expr a
 var v@(Variable (Atom x _)) = Expr (Var x) (symbolArity x) (\env -> unValuation env v)
diff --git a/src/Test/QuickSpec/TestTotality.hs b/src/Test/QuickSpec/TestTotality.hs
--- a/src/Test/QuickSpec/TestTotality.hs
+++ b/src/Test/QuickSpec/TestTotality.hs
@@ -17,6 +17,7 @@
 import Test.QuickSpec.Term hiding (symbols)
 import Test.QuickCheck
 import Test.QuickCheck.Gen
+import Test.QuickCheck.Random
 import System.Random
 import Control.Monad
 import Data.List hiding (lookup)
@@ -70,6 +71,6 @@
 
 always :: Sig -> Gen Bool -> IO Bool
 always sig x = do
-  gens <- replicateM 100 newStdGen
+  gens <- replicateM 100 newQCGen
   let sizes = cycle [0,2..maxQuickCheckSize sig]
   return (and [unGen x g n | (g, n) <- zip gens sizes])