diff --git a/Data/BatchedQueue.hs b/Data/BatchedQueue.hs
--- a/Data/BatchedQueue.hs
+++ b/Data/BatchedQueue.hs
@@ -83,7 +83,7 @@
   if not (ok (batchLabel batch)) then removeMinFilter ok (Queue q) else
     case unconsBatch batch of
       (entry, Just batch') ->
-        Just (entry, Queue (Heap.insert (Best batch') q))
+        Just (entry, Queue (Heap.insert (Best batch') q)) -- TODO: investigate if this can be made more efficient (removeMin+insert causes two merges even if the same batch is at the root before and after
       (entry, Nothing) ->
         Just (entry, Queue q)
 
diff --git a/Data/Intern.hs b/Data/Intern.hs
new file mode 100644
--- /dev/null
+++ b/Data/Intern.hs
@@ -0,0 +1,147 @@
+-- | Interning, annotating values with unique IDs.
+
+{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP, PatternSynonyms, ViewPatterns, ConstraintKinds #-}
+module Data.Intern(Intern, Sym, pattern Sym, intern, unintern, unsafeMkSym, symId) where
+
+import Data.IORef
+import System.IO.Unsafe
+import qualified Data.Map.Strict as Map
+import Data.Map.Strict(Map)
+import qualified Data.DynamicArray as DynamicArray
+import Data.DynamicArray(Array)
+import Data.Typeable
+import GHC.Exts
+import GHC.Int
+import Unsafe.Coerce
+
+-- | Type class constraints for a value to be internable.
+type Intern a = (Typeable a, Ord a)
+
+-- | An interned value of type @a@.
+newtype Sym a = MkSym Int32
+  deriving (Eq, Ord)
+
+instance Show a => Show (Sym a) where
+  show = show . unintern
+
+-- | The unique ID of a symbol.
+symId :: Sym a -> Int
+symId (MkSym x) = fromIntegral x
+
+type role Sym nominal -- no coercions please
+
+-- | Construct a @'Sym' a@ from its unique ID, which must be the 'symId' of
+-- an already existing 'Sym'. Extremely unsafe!
+unsafeMkSym :: Int -> Sym a
+unsafeMkSym = MkSym . fromIntegral
+
+-- The global cache of interned values.
+{-# NOINLINE cachesRef #-}
+cachesRef :: IORef Caches
+cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))
+
+data Caches =
+  Caches {
+    -- The next id number to assign.
+    caches_nextId :: {-# UNPACK #-} !Int32,
+    -- A map from values to IDs.
+    caches_from   :: !(Map TypeRep (Cache Any)),
+    -- The reverse map from IDs to values.
+    caches_to     :: !(Array Any) }
+
+type Cache a = Map a Int32
+
+atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a
+atomicModifyCaches f = do
+  -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the
+  -- compare-and-swap. This causes bad things to happen when 'intern'
+  -- is used reentrantly (i.e. the Ord instance itself calls intern).
+  -- This function only lets the swap happen if caches_nextId didn't
+  -- change (i.e., no new values were inserted).
+  !caches <- readIORef cachesRef
+  -- First compute the update.
+  let !(!caches', !x) = f caches
+  -- Now see if anyone else updated the cache in between
+  -- (can happen if f called 'intern', or in a concurrent setting).
+  ok <- atomicModifyIORef' cachesRef $ \cachesNow ->
+    if caches_nextId caches == caches_nextId cachesNow
+    then (caches', True)
+    else (cachesNow, False)
+  if ok then return x else atomicModifyCaches f
+
+-- Versions of unsafeCoerce with slightly more type checking
+toAnyCache :: Cache a -> Cache Any
+toAnyCache = unsafeCoerce
+
+fromAnyCache :: Cache Any -> Cache a
+fromAnyCache = unsafeCoerce
+
+toAny :: a -> Any
+toAny = unsafeCoerce
+
+fromAny :: Any -> a
+fromAny = unsafeCoerce
+
+-- | Intern a value.
+{-# NOINLINE intern #-}
+intern :: forall a. Intern a => a -> Sym a
+intern x =
+  unsafeDupablePerformIO $ do
+    -- Common case: symbol is already interned.
+    caches <- readIORef cachesRef
+    case tryFind caches of
+      Just s -> return s
+      Nothing -> do
+        -- Rare case: symbol has not yet been interned.
+        x <- atomicModifyCaches $ \caches ->
+          case tryFind caches of
+            Just s -> (caches, s)
+            Nothing ->
+              insert caches
+        return x
+
+  where
+    ty = typeOf x
+
+    tryFind :: Caches -> Maybe (Sym a)
+    tryFind Caches{..} =
+      MkSym <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)
+
+    insert :: Caches -> (Caches, Sym a)
+    insert caches@Caches{..} =
+      if n < 0 then error "label overflow" else
+      (caches {
+         caches_nextId = n+1,
+         caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,
+         caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },
+       MkSym n)
+      where
+        n = caches_nextId
+        cache =
+          fromAnyCache $
+          Map.findWithDefault Map.empty ty caches_from
+
+-- | Recover the underlying value from a 'Sym'.
+unintern :: Sym a -> a
+-- N.B. must force n before calling readIORef, otherwise a call of
+-- the form
+--   unintern (intern x)
+-- doesn't work.
+unintern (MkSym !(I32# n#)) = uninternWorker n#
+
+{-# NOINLINE uninternWorker #-}
+#if __GLASGOW_HASKELL__ >= 902
+uninternWorker :: Int32# -> a
+#else
+uninternWorker :: Int# -> a
+#endif
+uninternWorker n# =
+  unsafeDupablePerformIO $ do
+    let n = I32# n#
+    Caches{..} <- readIORef cachesRef
+    x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to)
+    return x
+
+pattern Sym :: Intern a => a -> Sym a
+pattern Sym x <- (unintern -> x) where
+  Sym x = intern x
diff --git a/Data/Label.hs b/Data/Label.hs
deleted file mode 100644
--- a/Data/Label.hs
+++ /dev/null
@@ -1,137 +0,0 @@
--- | Assignment of unique IDs to values.
--- Inspired by the 'intern' package.
-
-{-# LANGUAGE RecordWildCards, ScopedTypeVariables, BangPatterns, MagicHash, RoleAnnotations, CPP #-}
-module Data.Label(Label, unsafeMkLabel, labelNum, label, find) where
-
-import Data.IORef
-import System.IO.Unsafe
-import qualified Data.Map.Strict as Map
-import Data.Map.Strict(Map)
-import qualified Data.DynamicArray as DynamicArray
-import Data.DynamicArray(Array)
-import Data.Typeable
-import GHC.Exts
-import GHC.Int
-import Unsafe.Coerce
-
--- | A value of type @a@ which has been given a unique ID.
-newtype Label a =
-  Label {
-    -- | The unique ID of a label.
-    labelNum :: Int32 }
-  deriving (Eq, Ord, Show)
-
-type role Label nominal
-
--- | Construct a @'Label' a@ from its unique ID, which must be the 'labelNum' of
--- an already existing 'Label'. Extremely unsafe!
-unsafeMkLabel :: Int32 -> Label a
-unsafeMkLabel = Label
-
--- The global cache of labels.
-{-# NOINLINE cachesRef #-}
-cachesRef :: IORef Caches
-cachesRef = unsafePerformIO (newIORef (Caches 0 Map.empty DynamicArray.newArray))
-
-data Caches =
-  Caches {
-    -- The next id number to assign.
-    caches_nextId :: {-# UNPACK #-} !Int32,
-    -- A map from values to labels.
-    caches_from   :: !(Map TypeRep (Cache Any)),
-    -- The reverse map from labels to values.
-    caches_to     :: !(Array Any) }
-
-type Cache a = Map a Int32
-
-atomicModifyCaches :: (Caches -> (Caches, a)) -> IO a
-atomicModifyCaches f = do
-  -- N.B. atomicModifyIORef' ref f evaluates f ref *after* doing the
-  -- compare-and-swap. This causes bad things to happen when 'label'
-  -- is used reentrantly (i.e. the Ord instance itself calls label).
-  -- This function only lets the swap happen if caches_nextId didn't
-  -- change (i.e., no new values were inserted).
-  !caches <- readIORef cachesRef
-  -- First compute the update.
-  let !(!caches', !x) = f caches
-  -- Now see if anyone else updated the cache in between
-  -- (can happen if f called 'label', or in a concurrent setting).
-  ok <- atomicModifyIORef' cachesRef $ \cachesNow ->
-    if caches_nextId caches == caches_nextId cachesNow
-    then (caches', True)
-    else (cachesNow, False)
-  if ok then return x else atomicModifyCaches f
-
--- Versions of unsafeCoerce with slightly more type checking
-toAnyCache :: Cache a -> Cache Any
-toAnyCache = unsafeCoerce
-
-fromAnyCache :: Cache Any -> Cache a
-fromAnyCache = unsafeCoerce
-
-toAny :: a -> Any
-toAny = unsafeCoerce
-
-fromAny :: Any -> a
-fromAny = unsafeCoerce
-
--- | Assign a label to a value.
-{-# NOINLINE label #-}
-label :: forall a. (Typeable a, Ord a) => a -> Label a
-label x =
-  unsafeDupablePerformIO $ do
-    -- Common case: label is already there.
-    caches <- readIORef cachesRef
-    case tryFind caches of
-      Just l -> return l
-      Nothing -> do
-        -- Rare case: label was not there.
-        x <- atomicModifyCaches $ \caches ->
-          case tryFind caches of
-            Just l -> (caches, l)
-            Nothing ->
-              insert caches
-        return x
-
-  where
-    ty = typeOf x
-
-    tryFind :: Caches -> Maybe (Label a)
-    tryFind Caches{..} =
-      Label <$> (Map.lookup ty caches_from >>= Map.lookup x . fromAnyCache)
-
-    insert :: Caches -> (Caches, Label a)
-    insert caches@Caches{..} =
-      if n < 0 then error "label overflow" else
-      (caches {
-         caches_nextId = n+1,
-         caches_from = Map.insert ty (toAnyCache (Map.insert x n cache)) caches_from,
-         caches_to = DynamicArray.updateWithDefault undefined (fromIntegral n) (toAny x) caches_to },
-       Label n)
-      where
-        n = caches_nextId
-        cache =
-          fromAnyCache $
-          Map.findWithDefault Map.empty ty caches_from
-
--- | Recover the underlying value from a label.
-find :: Label a -> a
--- N.B. must force n before calling readIORef, otherwise a call of
--- the form
---   find (label x)
--- doesn't work.
-find (Label !(I32# n#)) = findWorker n#
-
-{-# NOINLINE findWorker #-}
-#if __GLASGOW_HASKELL__ >= 902
-findWorker :: Int32# -> a
-#else
-findWorker :: Int# -> a
-#endif
-findWorker n# =
-  unsafeDupablePerformIO $ do
-    let n = I32# n#
-    Caches{..} <- readIORef cachesRef
-    x <- return $! fromAny (DynamicArray.getWithDefault undefined (fromIntegral n) caches_to)
-    return x
diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -56,6 +56,7 @@
     cfg_max_critical_pairs        :: Int64,
     cfg_max_cp_depth              :: Int,
     cfg_max_rules                 :: Int,
+    cfg_max_time                  :: Maybe Double,
     cfg_simplify                  :: Bool,
     cfg_renormalise_percent       :: Int,
     cfg_cp_sample_size            :: Int,
@@ -63,7 +64,7 @@
     cfg_set_join_goals            :: Bool,
     cfg_always_simplify           :: Bool,
     cfg_complete_subsets          :: Bool,
-    cfg_score_cp                  :: Depth -> Equation f -> Float,
+    cfg_score_cp                  :: Depth -> Index f (Hint f) -> Equation f -> Float,
     cfg_join                      :: Join.Config,
     cfg_proof_presentation        :: Proof.Config f,
     cfg_eliminate_axioms          :: [Axiom f],
@@ -71,7 +72,10 @@
     cfg_random_mode_goal_directed :: Bool,
     cfg_random_mode_simple        :: Bool,
     cfg_random_mode_best_of       :: Int,
-    cfg_always_complete           :: Bool }
+    cfg_always_complete           :: Bool,
+    cfg_hint_skel_cost            :: Float,
+    cfg_hint_skel_factor          :: Float,
+    cfg_print_score               :: Bool }
 
 -- | The prover state.
 data State f =
@@ -82,6 +86,7 @@
     st_joinable       :: !(Index f (Equation f)),
     st_goals          :: ![Goal f],
     st_queue          :: !(Queue Batch),
+    st_hints          :: !(Index f (Hint f)),
     st_next_active    :: {-# UNPACK #-} !Id,
     st_considered     :: {-# UNPACK #-} !Int64,
     st_simplified_at  :: {-# UNPACK #-} !Id,
@@ -100,6 +105,7 @@
     cfg_max_critical_pairs = maxBound,
     cfg_max_cp_depth = maxBound,
     cfg_max_rules = maxBound,
+    cfg_max_time = Nothing,
     cfg_simplify = True,
     cfg_renormalise_percent = 5,
     cfg_renormalise_threshold = 20,
@@ -107,7 +113,7 @@
     cfg_set_join_goals = True,
     cfg_always_simplify = False,
     cfg_complete_subsets = False,
-    cfg_score_cp = \d eqn -> fromIntegral (score CP.defaultConfig d eqn),
+    cfg_score_cp = \d hints eqn -> score CP.defaultConfig d hints eqn,
     cfg_join = Join.defaultConfig,
     cfg_proof_presentation = Proof.defaultConfig,
     cfg_eliminate_axioms = [],
@@ -115,12 +121,16 @@
     cfg_random_mode_goal_directed = False,
     cfg_random_mode_best_of = 1,
     cfg_random_mode_simple = False,
-    cfg_always_complete = False }
+    cfg_always_complete = False,
+    cfg_hint_skel_cost = 1,
+    cfg_hint_skel_factor = 0,
+    cfg_print_score = False }
 
 -- | Does this configuration run the prover in a complete mode?
 configIsComplete :: Config f -> Bool
 configIsComplete Config{..} =
-  isNothing (cfg_accept_term) &&
+  isNothing cfg_accept_term &&
+  isNothing cfg_max_time &&
   cfg_max_critical_pairs == maxBound &&
   cfg_max_cp_depth == maxBound &&
   cfg_max_rules == maxBound
@@ -135,6 +145,7 @@
     st_joinable = Index.empty,
     st_goals = [],
     st_queue = Queue.empty,
+    st_hints = Index.empty,
     st_next_active = 1,
     st_considered = 0,
     st_simplified_at = 1,
@@ -155,7 +166,7 @@
 -- | A message which is produced by the prover when something interesting happens.
 data Message f =
     -- | A new rule.
-    NewActive !(Active f)
+    NewActive !(Maybe Float) !(Active f)
     -- | A new joinable equation.
   | NewEquation !(Equation f)
     -- | A rule was deleted.
@@ -172,7 +183,10 @@
   | NewProblemTerm !(ConfluenceFailure f)
 
 instance Function f => Pretty (Message f) where
-  pPrint (NewActive rule) = pPrint rule
+  pPrint (NewActive mscore rule) =
+    case mscore of
+      Nothing -> pPrint rule
+      Just score -> parens (pPrint score) <+> pPrint rule
  --   $$ case cp_top (active_cp rule) of { Just t -> text "  (normal forms of term" <+> pPrint t <#> text ")"; Nothing -> pPrintEmpty }
   pPrint (NewEquation eqn) =
     text "  (hard)" <+> pPrint eqn
@@ -225,10 +239,10 @@
 makePassives :: Function f => Config f -> State f -> Active f -> [Passive]
 -- don't generate critical pairs when in random mode
 makePassives Config{cfg_random_mode = True} _ _ = []
-makePassives config@Config{..} State{..} rule =
+makePassives config@Config{..} state@State{..} rule =
 -- XXX factor out depth calculation
   stampWith "make critical pair" length
-  [ makePassive config overlap
+  [ makePassive config state overlap
   | ok rule,
     overlap <- overlaps (index_oriented st_rules) (filter ok rules) rule ]
   where
@@ -296,10 +310,10 @@
   batchSize Batch{..} = 1 + PackedSequence.size batch_rest
 
 {-# INLINEABLE makePassive #-}
-makePassive :: Function f => Config f -> Overlap (Active f) f -> Passive
-makePassive Config{..} Overlap{..} =
+makePassive :: Function f => Config f -> State f -> Overlap (Active f) f -> Passive
+makePassive Config{..} State{..} Overlap{..} =
   Passive {
-    passive_score = cfg_score_cp depth overlap_eqn,
+    passive_score = cfg_score_cp depth st_hints overlap_eqn,
     passive_rule1 = active_id overlap_rule1,
     passive_rule2 = active_id overlap_rule2,
     passive_how   = overlap_how }
@@ -328,7 +342,7 @@
     passive_score =
       passive_score passive `min`
       -- XXX factor out depth calculation
-      cfg_score_cp (succ (the r1 `max` the r2)) (overlap_eqn overlap) }
+      cfg_score_cp (succ (the r1 `max` the r2)) st_hints (overlap_eqn overlap) }
 
 -- | Check if we should renormalise the queue.
 {-# INLINEABLE shouldSimplifyQueue #-}
@@ -407,6 +421,10 @@
     cp_top = active_top,
     cp_proof = derivation active_proof }
 
+activeScore :: Config f -> State f -> Active f -> Float
+activeScore Config{..} State{..} Active{..} =
+  cfg_score_cp (info_depth active_info) st_hints (equation active_proof)
+
 activeRules :: Active f -> [Rule f]
 activeRules Active{..} =
   case active_positions of
@@ -436,8 +454,11 @@
 addActive config state@State{..} active0 =
   let
     active@Active{..} = active0 st_next_active
+    mscore
+      | cfg_print_score config = Just (activeScore config state active)
+      | otherwise = Nothing
     state' =
-      message (NewActive active) $
+      message (NewActive mscore active) $
       addActiveOnly state{st_next_active = st_next_active+1} active
   in if subsumed (st_joinable, st_complete) st_rules (unorient active_rule) then
     state
@@ -497,6 +518,16 @@
     insertRule rules rule =
       RuleIndex.insert (lhs rule) rule rules
 
+-- Add an active without generating critical pairs. Used in interreduction.
+{-# INLINEABLE addActiveSimp #-}
+addActiveSimp :: Function f => State f -> Active f -> State f
+addActiveSimp state@State{..} active@Active{..} =
+  state {
+    st_rules = foldl' insertRule st_rules (activeRules active) }
+  where
+    insertRule rules rule =
+      RuleIndex.insert (lhs rule) rule rules
+
 -- Delete an active. Used in interreduction, not suitable for general use.
 {-# INLINE deleteActive #-}
 deleteActive :: Function f => State f -> Active f -> State f
@@ -578,6 +609,16 @@
       cp_top = Nothing,
       cp_proof = Proof.axiom axiom }
 
+-- Add a new hint.
+{-# INLINEABLE addHint #-}
+addHint :: Function f => Config f -> State f -> Term f -> State f
+addHint Config{..} state@State{..} hint =
+  state { st_hints = Index.insert hint (Hint hint cost) st_hints }
+  where
+    cost = fromIntegral (len hint - length (vars hint)) * cfg_hint_skel_factor + cfg_hint_skel_cost +
+      -- Add a cost for duplicated variables (since they only get counted once otherwise)
+      fromIntegral (length (vars hint) - length (usort (vars hint)))
+
 -- Record an equation as being joinable.
 {-# INLINEABLE addJoinable #-}
 addJoinable :: Function f => State f -> Equation f -> State f
@@ -754,11 +795,13 @@
       (Just active_model) (active_cp active)
   of
     Right (_, cps) ->
+      flip addActiveSimp active $
       flip (foldl' (\state cp -> consider config state active_info cp)) cps $
       message (DeleteActive active) $
       deleteActive state active
     Left (cp, model)
       | cp_eqn cp `simplerThan` cp_eqn (active_cp active) ->
+        flip addActiveSimp active $
         flip (foldl' (\state cp -> consider config state active_info cp)) (split cp) $
         message (DeleteActive active) $
         deleteActive state active
@@ -805,6 +848,13 @@
           let !n = Queue.size st_queue
           lift $ output_message (Status n)]
 
+    checkTimeout <-
+      case cfg_max_time of
+        Nothing -> return (return False)
+        Just timeout -> do
+          task <- newTask timeout 100 (return ())
+          return $ fmap isJust (checkTask task)
+
     let
       loop = do
         progress <- StateM.state (complete1 config)
@@ -816,7 +866,8 @@
         lift $ mapM_ output_message (messages state)
         StateM.put (clearMessages state)
         mapM_ checkTask tasks
-        when progress loop
+        timedOut <- checkTimeout
+        when (progress && not timedOut) loop
 
     loop
 
@@ -898,7 +949,7 @@
         Nothing ->
           trace ("Overlap " ++ prettyShow (overlap_eqn o) ++ " was spurious") Nothing -- should be rare
         Just o' ->
-          Just (cfg_score_cp config 0 (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))
+          Just (cfg_score_cp config 0 (st_hints state) (overlap_eqn o'), (Info 0 IntSet.empty, makeCriticalPair o, changed, cf))
 
 -- Return all goal terms. Handles the $equals coding.
 goalTerms :: Function f => State f -> [Term f]
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -1,18 +1,18 @@
 -- | Useful operations on terms and similar. Also re-exports some generally
 -- useful modules such as 'Twee.Term' and 'Twee.Pretty'.
 
-{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns #-}
+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances, DeriveFunctor, DefaultSignatures, FlexibleContexts, TypeOperators, MultiParamTypeClasses, GeneralizedNewtypeDeriving, ConstraintKinds, RecordWildCards, BangPatterns, PatternSynonyms #-}
 module Twee.Base(
   -- * Re-exported functionality
   module Twee.Term, module Twee.Pretty,
   -- * The 'Symbolic' typeclass
   Symbolic(..), subst, terms,
-  TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, FunOf,
+  TermOf, TermListOf, SubstOf, TriangleSubstOf, BuilderOf, SymOf,
   vars, isGround, funs, occ, occVar, occs, nests, canonicalise, renameAvoiding, renameManyAvoiding, freshVar,
   -- * General-purpose functionality
-  Id(..), Has(..),
+  Id(..), Has(..), Intern, Sym, pattern Sym,
   -- * Typeclasses
-  Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground,
+  Minimal(..), minimalTerm, isMinimal, erase, eraseExcept, ground, skolemise,
   Ordered(..), lessThan, orientTerms,
   EqualsBonus(..), isTrueTerm, isFalseTerm, decodeEquality,
   Strictness(..), Function) where
@@ -31,6 +31,7 @@
 import Data.Maybe
 import qualified Data.IntMap.Strict as IntMap
 import Data.Serialize
+import Data.Intern
 
 -- | Represents a unique identifier (e.g., for a rule).
 newtype Id = Id { unId :: Int32 }
@@ -72,7 +73,7 @@
 -- | A builder compatible with a given 'Symbolic'.
 type BuilderOf a = Builder (ConstantOf a)
 -- | The underlying type of function symbols of a given 'Symbolic'.
-type FunOf a = Fun (ConstantOf a)
+type SymOf a = Sym (ConstantOf a)
 
 instance Symbolic (Term f) where
   type ConstantOf (Term f) = f
@@ -136,12 +137,12 @@
 
 -- | Find the function symbols occurring in the argument.
 {-# INLINE funs #-}
-funs :: Symbolic a => a -> [FunOf a]
+funs :: Symbolic a => a -> [SymOf a]
 funs x = [ f | t <- DList.toList (termsDL x), App f _ <- subtermsList t ]
 
 -- | Count how many times a function symbol occurs in the argument.
 {-# INLINE occ #-}
-occ :: Symbolic a => FunOf a -> a -> Int
+occ :: Symbolic a => SymOf a -> a -> Int
 occ x t = length (filter (== x) (funs t))
 
 -- | Count how many times a variable occurs in the argument.
@@ -154,7 +155,7 @@
 occs :: Symbolic a => a -> IntMap.IntMap Int
 occs = foldl' insert IntMap.empty . funs
   where
-    insert !m !f = IntMap.insertWith (+) (fun_id f) 1 m
+    insert !m !f = IntMap.insertWith (+) (symId f) 1 m
 
 -- | 'nest' from Fuchs, "The application of goal-oriented heuristics
 -- for proving equational theorems via the unfailing Knuth-Bendix
@@ -165,11 +166,11 @@
 
 -- helper function for nests
 hnest :: Int -> Int -> IntMap.IntMap Int -> TermList f -> IntMap.IntMap Int
-hnest !f !c !as Empty = IntMap.insertWith max f c as
+hnest !f !c !as Nil = IntMap.insertWith max f c as
 hnest f c as (Cons (Var _) ts) = hnest f c as ts
-hnest f c as (Cons (App _ Empty) ts) = hnest f c as ts
+hnest f c as (Cons (App _ Nil) ts) = hnest f c as ts
 hnest f c as (Cons (App g ts) us) =
-  let as' = hnest (fun_id g) (if f == fun_id g then c+1 else 1) as ts
+  let as' = hnest (symId g) (if f == symId g then c+1 else 1) as ts
   in hnest f c as' us
 
 -- | Rename the argument so that variables are introduced in a canonical order
@@ -214,7 +215,7 @@
   
 -- | Check if a term is the minimal constant.
 isMinimal :: Minimal f => Term f -> Bool
-isMinimal (App f Empty) | f == minimal = True
+isMinimal (App f Nil) | f == minimal = True
 isMinimal _ = False
 
 -- | Build the minimal constant as a term.
@@ -239,10 +240,14 @@
 ground :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
 ground t = erase (vars t) t
 
+-- | Skolemise the argument.
+skolemise :: (Symbolic a, ConstantOf a ~ f, Minimal f) => a -> a
+skolemise t = subst (\(V x) -> con (skolem x)) t
+
 -- | For types which have a notion of size.
 -- | The collection of constraints which the type of function symbols must
 -- satisfy in order to be used by twee.
-type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Labelled f)
+type Function f = (Ordered f, Minimal f, PrettyTerm f, EqualsBonus f, Intern f)
 
 -- | A hack for encoding Horn clauses. See 'Twee.CP.Score'.
 -- The default implementation of 'hasEqualsBonus' should work OK.
@@ -254,20 +259,20 @@
   isTrue _ = False
   isFalse _ = False
 
-isFalseTerm, isTrueTerm :: (EqualsBonus f, Labelled f) => Term f -> Bool
+isFalseTerm, isTrueTerm :: (EqualsBonus f, Intern f) => Term f -> Bool
 isFalseTerm (App false _) = isFalse false
 isFalseTerm _ = False
 isTrueTerm (App true _) = isTrue true
 isTrueTerm _ = False
 
 -- Decode $equals(t,u) into an equation t=u.
-decodeEquality :: (EqualsBonus f, Labelled f) => Term f -> Maybe (Term f, Term f)
-decodeEquality (App equals (Cons t (Cons u Empty)))
+decodeEquality :: (EqualsBonus f, Intern f) => Term f -> Maybe (Term f, Term f)
+decodeEquality (App equals (Cons t (Cons u Nil)))
   | isEquals equals = Just (t, u)
 decodeEquality _ = Nothing
 
-instance (Labelled f, EqualsBonus f) => EqualsBonus (Fun f) where
-  hasEqualsBonus = hasEqualsBonus . fun_value
-  isEquals = isEquals . fun_value
-  isTrue = isTrue . fun_value
-  isFalse = isFalse . fun_value
+instance (Intern f, EqualsBonus f) => EqualsBonus (Sym f) where
+  hasEqualsBonus = hasEqualsBonus . unintern
+  isEquals = isEquals . unintern
+  isTrue = isTrue . unintern
+  isFalse = isFalse . unintern
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -6,6 +6,7 @@
 import Twee.Base
 import Twee.Rule
 import Twee.Index(Index)
+import qualified Twee.Index as Index
 import qualified Data.Set as Set
 import Control.Monad
 import Data.List hiding (singleton)
@@ -18,6 +19,7 @@
 import Data.Bits
 import Data.Serialize
 import Data.Int
+--import Debug.Trace
 
 -- | The set of positions at which a term can have critical overlaps.
 data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
@@ -33,7 +35,7 @@
 positions t = aux 0 Set.empty (singleton t)
   where
     -- Consider only general superpositions.
-    aux !_ !_ Empty = NilP
+    aux !_ !_ Nil = NilP
     aux n m (Cons (Var _) t) = aux (n+1) m t
     aux n m ConsSym{hd = t@App{}, rest = u}
       | t `Set.member` m = aux (n+1) m u
@@ -196,25 +198,37 @@
 -- | The configuration for the critical pair weighting heuristic.
 data Config =
   Config {
-    cfg_lhsweight :: !Int,
-    cfg_rhsweight :: !Int,
-    cfg_funweight :: !Int,
-    cfg_varweight :: !Int,
-    cfg_depthweight :: !Int,
-    cfg_dupcost :: !Int,
-    cfg_dupfactor :: !Int }
+    cfg_lhsweight :: !Float,
+    cfg_rhsweight :: !Float,
+    cfg_funweight :: !Float,
+    cfg_varweight :: !Float,
+    cfg_depthweight :: !Float,
+    cfg_dupcost :: !Float,
+    cfg_dupfactor :: !Float,
+    cfg_resonance :: !Bool }
 
+data Hint f =
+  Hint {
+    hint_term :: {-# UNPACK #-} !(Term f),
+    hint_cost :: {-# UNPACK #-} !Float }
+
+instance Symbolic (Hint f) where
+  type ConstantOf (Hint f) = f
+  termsDL Hint{..} = termsDL hint_term
+  subst_ sub (Hint t c) = Hint (subst_ sub t) c
+
 -- | The default heuristic configuration.
 defaultConfig :: Config
 defaultConfig =
   Config {
     cfg_lhsweight = 4,
     cfg_rhsweight = 1,
-    cfg_funweight = 7,
-    cfg_varweight = 6,
-    cfg_depthweight = 16,
-    cfg_dupcost = 7,
-    cfg_dupfactor = 0 }
+    cfg_funweight = 1,
+    cfg_varweight = 6/7,
+    cfg_depthweight = 2,
+    cfg_dupcost = 1,
+    cfg_dupfactor = 0,
+    cfg_resonance = False }
 
 -- | Compute a score for a critical pair.
 
@@ -223,31 +237,40 @@
 -- where l is the biggest term and r is the smallest,
 -- and variables have weight 1 and functions have weight cfg_funweight.
 {-# INLINEABLE score #-}
-score :: Function f => Config -> Depth -> Equation f -> Int
-score Config{..} depth (l :=: r) =
+score :: Function f => Config -> Depth -> Index f (Hint f) -> Equation f -> Float
+score Config{..} depth hints (l :=: r) =
   fromIntegral depth * cfg_depthweight +
   (m + n) * cfg_rhsweight +
-  intMax m n * (cfg_lhsweight - cfg_rhsweight)
+  max m n * (cfg_lhsweight - cfg_rhsweight)
   where
-    m = size' 0 (singleton l)
-    n = size' 0 (singleton r)
+    m = size' 0 (singleton l) []
+    n = size' 0 (singleton r) []
 
-    size' !n Empty = n
-    size' n (Cons t ts)
-      | len t > 1, t `isSubtermOfList` ts =
-        size' (n+cfg_dupcost+cfg_dupfactor*len t) ts
-    size' n ts
+    size' !_ !_ !_ | False = undefined
+    size' n Nil ts =
+      case ts of
+        [] -> n
+        u:us -> size' n u us
+    size' n (Cons t ts) us
+      | len t > 1, t `isSubtermOfList` ts || any (t `isSubtermOfList`) us =
+        size' (n+cfg_dupcost+cfg_dupfactor*fromIntegral (len t)) ts us
+    size' n (Cons t ts) us
+      | len t > 1, (sub, Hint{..}):_ <- Index.matches t hints,
+        not cfg_resonance || allSubst (\_ t -> case t of { UnsafeCons (Var _) _ -> True; _ -> False }) sub =
+        size' (n + hint_cost) ts (map snd (Term.substToList' sub) ++ us)
+        --trace ("hint: len " ++ show (len t) ++ ", new cost " ++ show new_cost ++ ": " ++ prettyShow t) $
+    size' n ts xs
       | Cons (App f ws@(Cons a (Cons b us))) vs <- ts,
         not (isVar a),
         not (isVar b),
-        hasEqualsBonus (fun_value f),
+        hasEqualsBonus f,
         Just sub <- unify a b =
-        size' (n+cfg_funweight) ws `min`
-        size' (size' (n+1) (subst sub us)) (subst sub vs)
-    size' n (Cons (Var _) ts) =
-      size' (n+cfg_varweight) ts
-    size' n ConsSym{hd = App{}, rest = ts} =
-      size' (n+cfg_funweight) ts
+        size' (n+cfg_funweight) ws xs `min`
+        size' (n+1) (subst sub us) (subst sub (vs:xs))
+    size' n (Cons (Var _) ts) us =
+      size' (n+cfg_varweight) ts us
+    size' n ConsSym{hd = App{}, rest = ts} us =
+      size' (n+cfg_funweight) ts us
 
 ----------------------------------------------------------------------
 -- * Higher-level handling of critical pairs.
@@ -274,7 +297,7 @@
       cp_top = subst_ sub cp_top,
       cp_proof = subst_ sub cp_proof }
 
-instance (Labelled f, PrettyTerm f) => Pretty (CriticalPair f) where
+instance (Intern f, PrettyTerm f) => Pretty (CriticalPair f) where
   pPrint CriticalPair{..} =
     vcat [
       pPrint cp_eqn,
diff --git a/Twee/Constraints.hs b/Twee/Constraints.hs
--- a/Twee/Constraints.hs
+++ b/Twee/Constraints.hs
@@ -14,15 +14,19 @@
 import Data.Map.Strict(Map)
 import Data.Ord
 import Twee.Term hiding (lookup)
+import Test.QuickCheck(shuffle)
+import Test.QuickCheck.Gen(unGen)
+import Test.QuickCheck.Random(mkQCGen)
+import Data.Intern
 
-data Atom f = Constant (Fun f) | Variable Var deriving (Show, Eq, Ord)
+data Atom f = Constant (Sym f) | Variable Var deriving (Show, Eq, Ord)
 
 {-# INLINE atoms #-}
 atoms :: Term f -> [Atom f]
 atoms t = aux (singleton t)
   where
-    aux Empty = []
-    aux (Cons (App f Empty) t) = Constant f:aux t
+    aux Nil = []
+    aux (Cons (App f Nil) t) = Constant f:aux t
     aux (Cons (Var x) t) = Variable x:aux t
     aux ConsSym{rest = t} = aux t
 
@@ -31,11 +35,11 @@
 toTerm (Variable x) = build (var x)
 
 fromTerm :: Flat.Term f -> Maybe (Atom f)
-fromTerm (App f Empty) = Just (Constant f)
+fromTerm (App f Nil) = Just (Constant f)
 fromTerm (Var x) = Just (Variable x)
 fromTerm _ = Nothing
 
-instance (Labelled f, PrettyTerm f) => Pretty (Atom f) where
+instance (Intern f, PrettyTerm f) => Pretty (Atom f) where
   pPrint = pPrint . toTerm
 
 data Formula f =
@@ -45,7 +49,7 @@
   | Or  [Formula f]
   deriving (Eq, Ord, Show)
 
-instance (Labelled f, PrettyTerm f) => Pretty (Formula f) where
+instance (Intern f, PrettyTerm f) => Pretty (Formula f) where
   pPrintPrec _ _ (Less t u) = hang (pPrint t <+> text "<") 2 (pPrint u)
   pPrintPrec _ _ (LessEq t u) = hang (pPrint t <+> text "<=") 2 (pPrint u)
   pPrintPrec _ _ (And []) = text "true"
@@ -98,12 +102,12 @@
 data Branch f =
   -- Branches are kept normalised wrt equals
   Branch {
-    funs        :: [Fun f],
+    funs        :: [Sym f],
     less        :: [(Atom f, Atom f)],  -- sorted
     equals      :: [(Atom f, Atom f)] } -- sorted, greatest atom first in each pair
   deriving (Eq, Ord)
 
-instance (Labelled f, PrettyTerm f) => Pretty (Branch f) where
+instance (Intern f, PrettyTerm f) => Pretty (Branch f) where
   pPrint Branch{..} =
     braces $ fsep $ punctuate (text ",") $
       [pPrint x <+> text "<" <+> pPrint y | (x, y) <- less ] ++
@@ -115,7 +119,7 @@
 norm :: Eq f => Branch f -> Atom f -> Atom f
 norm Branch{..} x = fromMaybe x (lookup x equals)
 
-contradictory :: (Minimal f, Ord f, Labelled f) => Branch f -> Bool
+contradictory :: (Minimal f, Ord f, Intern f) => Branch f -> Bool
 contradictory Branch{..} =
   or [f == minimal | (_, Constant f) <- less] ||
   or [f /= g | (Constant f, Constant g) <- equals] ||
@@ -125,7 +129,7 @@
     cyclic (AcyclicSCC _) = False
     cyclic (CyclicSCC _) = True
 
-formAnd :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f] -> [Branch f]
+formAnd :: (Minimal f, Ordered f, Intern f) => Formula f -> [Branch f] -> [Branch f]
 formAnd f bs = usort (bs >>= add f)
   where
     add (Less t u) b = addLess t u b
@@ -134,7 +138,7 @@
     add (And (f:fs)) b = add f b >>= add (And fs)
     add (Or fs) b = usort (concat [ add f b | f <- fs ])
 
-branches :: (Minimal f, Ordered f, Labelled f) => Formula f -> [Branch f]
+branches :: (Minimal f, Ordered f, Intern f) => Formula f -> [Branch f]
 branches x = aux [x]
   where
     aux [] = [Branch [] [] []]
@@ -146,7 +150,7 @@
       concatMap (addLess t u) (aux xs) ++
       concatMap (addEquals u t) (aux xs)
 
-addLess :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
+addLess :: (Minimal f, Ordered f, Intern f) => Atom f -> Atom f -> Branch f -> [Branch f]
 addLess _ (Constant min) _ | min == minimal = []
 addLess (Constant min) _ b | min == minimal = [b]
 addLess t0 u0 b@Branch{..} =
@@ -156,7 +160,7 @@
     t = norm b t0
     u = norm b u0
 
-addEquals :: (Minimal f, Ordered f, Labelled f) => Atom f -> Atom f -> Branch f -> [Branch f]
+addEquals :: (Minimal f, Ordered f, Intern f) => Atom f -> Atom f -> Branch f -> [Branch f]
 addEquals t0 u0 b@Branch{..}
   | t == u || (t, u) `elem` equals = [b]
   | otherwise =
@@ -172,7 +176,7 @@
       | x == t = u
       | otherwise = x
 
-addTerm :: (Minimal f, Ordered f, Labelled f) => Atom f -> Branch f -> Branch f
+addTerm :: (Minimal f, Ordered f, Intern f) => Atom f -> Branch f -> Branch f
 addTerm (Constant f) b
   | f `notElem` funs b =
     b {
@@ -189,7 +193,7 @@
 -- x <  y if major x < major y
 -- x <= y if major x = major y and minor x < minor y
 
-instance (Labelled f, PrettyTerm f) => Pretty (Model f) where
+instance (Intern f, PrettyTerm f) => Pretty (Model f) where
   pPrint (Model m)
     | Map.size m <= 1 = text "empty"
     | otherwise = fsep (go (sortBy (comparing snd) (Map.toList m)))
@@ -233,7 +237,14 @@
 varInModel :: (Minimal f, Ord f) => Model f -> Var -> Bool
 varInModel (Model m) x = Variable x `Map.member` m
 
-varGroups :: (Minimal f, Ord f) => Model f -> [(Fun f, [Var], Maybe (Fun f))]
+modelVarMaxBound :: Model f -> Int
+modelVarMaxBound (Model m) =
+  maximum (0:map (succ . fst) (Map.elems m))
+
+modelVarValue :: Model f -> Var -> Maybe Var
+modelVarValue (Model m) x = V . fst <$> Map.lookup (Variable x) m
+
+varGroups :: (Minimal f, Ord f) => Model f -> [(Sym f, [Var], Maybe (Sym f))]
 varGroups (Model m) = filter nonempty (go minimal (map fst (sortBy (comparing snd) (Map.toList m))))
   where
     go f xs =
@@ -248,10 +259,11 @@
     nonempty _ = True
 
 class Minimal f where
-  minimal :: Fun f
+  minimal :: Sym f
+  skolem :: Int -> Sym f
 
 {-# INLINE lessEqInModel #-}
-lessEqInModel :: (Minimal f, Ordered f, Labelled f) => Model f -> Atom f -> Atom f -> Maybe Strictness
+lessEqInModel :: (Minimal f, Ordered f, Intern f) => Model f -> Atom f -> Atom f -> Maybe Strictness
 lessEqInModel (Model m) x y
   | Just (a, _) <- Map.lookup x m,
     Just (b, _) <- Map.lookup y m,
@@ -264,7 +276,7 @@
   | Constant a <- x, a == minimal = Just Nonstrict
   | otherwise = Nothing
 
-solve :: (Minimal f, Ordered f, PrettyTerm f, Labelled f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
+solve :: (Minimal f, Ordered f, PrettyTerm f, Intern f) => [Atom f] -> Branch f -> Either (Model f) (Subst f)
 solve xs branch@Branch{..}
   | null equals && not (all true less) =
     error $ "Model " ++ prettyShow model ++ " is not a model of " ++ prettyShow branch ++ " (edges = " ++ prettyShow edges ++ ", vs = " ++ prettyShow vs ++ ")"
@@ -274,8 +286,9 @@
       sub = fromMaybe undefined . listToSubst $
         [(x, toTerm y) | (Variable x, y) <- equals] ++
         [(y, toTerm x) | (x@Constant{}, Variable y) <- equals]
-      vs = Constant minimal:reverse (flattenSCCs (stronglyConnComp edges))
+      vs = Constant minimal:reverse (flattenSCCs (stronglyConnComp edges'))
       edges = [(x, x, [y | (x', y) <- less', x == x']) | x <- as, x /= Constant minimal]
+      edges' = unGen (shuffle edges) (mkQCGen 12345) 0
       less' = less ++ [(Constant x, Constant y) | Constant x <- as, Constant y <- as, x << y]
       as = usort $ xs ++ map fst less ++ map snd less
       model = modelFromOrder vs
diff --git a/Twee/Equation.hs b/Twee/Equation.hs
--- a/Twee/Equation.hs
+++ b/Twee/Equation.hs
@@ -21,7 +21,7 @@
   termsDL (t :=: u) = termsDL t `mplus` termsDL u
   subst_ sub (t :=: u) = subst_ sub t :=: subst_ sub u
 
-instance (Labelled f, PrettyTerm f) => Pretty (Equation f) where
+instance (Intern f, PrettyTerm f) => Pretty (Equation f) where
   pPrint (x :=: y) = pPrint x <+> text "=" <+> pPrint y
 
 -- | Order an equation roughly left-to-right, and
@@ -32,15 +32,15 @@
   -- If the two terms have the same skeleton,
   -- then take whichever orientation gives a simpler equation
   | gl == gr =
-    let eq1 = canonicalise (l :=: r)
-        eq2 = canonicalise (r :=: l) in
     if eq1 == eq2 || orderedSimplerThan eq1 eq2 then eq1 else eq2
   -- Otherwise, the LHS should be the term with the greater skeleton
-  | gl `lessEq` gr = r :=: l
-  | otherwise = l :=: r
+  | gl `lessEq` gr = eq2
+  | otherwise = eq1
   where
     gl = ground l
     gr = ground r
+    eq1 = canonicalise (l :=: r)
+    eq2 = canonicalise (r :=: l)
 
 -- Helper for 'order' and 'simplerThan'
 orderedSimplerThan :: Function f => Equation f -> Equation f -> Bool
diff --git a/Twee/Index.hs b/Twee/Index.hs
--- a/Twee/Index.hs
+++ b/Twee/Index.hs
@@ -22,12 +22,14 @@
   delete,
   lookup,
   matches,
+  member,
   elems,
   fromList,
   fromListWith,
   invariant) where
 
 import Prelude hiding (null, lookup)
+import qualified Prelude (null)
 import Twee.Base hiding (var, fun, empty, singleton, prefix, funs, lookupList, lookup, at)
 import qualified Twee.Term as Term
 import Data.DynamicArray hiding (singleton)
@@ -36,8 +38,8 @@
 import Data.Numbered(Numbered)
 import qualified Data.Numbered as Numbered
 import qualified Data.IntMap.Strict as IntMap
-import qualified Twee.Term.Core as Core
 import Twee.Profile
+import Data.Intern
 
 -- The term index in this module is a _perfect discrimination tree_.
 -- This is a trie whose keys are terms, represented as flat lists of symbols
@@ -93,26 +95,26 @@
     -- The array is indexed by function number.
     fun      :: {-# UNPACK #-} !(Array (Index f a)),
     -- List of variable edges indexed by variable number.
-    -- Invariant: all edges present in the list are non-Nil.
+    -- Invariant: all edges present in the list are non-Empty.
     --
     -- Invariant: variables in terms are introduced in ascending
     -- order, with no gaps (i.e. if the term so far has the variables
     -- x1..xn, then the edges here must be drawn from x1...x{n+1}).
     var      :: {-# UNPACK #-} !(Numbered (Index f a)) } |
   -- An empty index.
-  Nil
+  Empty
   deriving Show
 
 minSize :: Index f a -> Int
-minSize Nil = maxBound
+minSize Empty = maxBound
 minSize idx = minSize_ idx
 
 -- | Check the invariant of an index. For debugging purposes.
 invariant :: Index f a -> Bool
-invariant Nil = True
+invariant Empty = True
 invariant Index{..} =
   nonEmpty &&
-  noNilVars &&
+  noEmptyVars &&
   maxPrefix &&
   sizeCorrect &&
   all invariant (map snd (toList fun)) &&
@@ -122,7 +124,7 @@
       not (List.null here) ||
       not (List.null (filter (not . null . snd) (toList fun))) ||
       not (List.null (Numbered.toList var))
-    noNilVars = -- the var field should not contain any Nils
+    noEmptyVars = -- the var field should not contain any Emptys
       all (not . null . snd) (Numbered.toList var)
     maxPrefix -- prefix should be used if possible
       | List.null here =
@@ -137,15 +139,15 @@
       | otherwise =
         minSize_ == lenList prefix
 
-instance Default (Index f a) where def = Nil
+instance Default (Index f a) where def = Empty
 
 -- | An empty index.
 empty :: Index f a
-empty = Nil
+empty = Empty
 
 -- | Is the index empty?
 null :: Index f a -> Bool
-null Nil = True
+null Empty = True
 null _ = False
 
 -- | An index with one entry.
@@ -154,12 +156,12 @@
 
 -- A leaf node, perhaps with a prefix.
 leaf :: TermList f -> [a] -> Index f a
-leaf !_ [] = Nil
+leaf !_ [] = Empty
 leaf t xs = Index (lenList t) t xs newArray Numbered.empty
 
 -- Add a prefix (given as a list of symbols) to all terms in an index.
 addPrefix :: [Term f] -> Index f a -> Index f a
-addPrefix _ Nil = Nil
+addPrefix _ Empty = Empty
 addPrefix [] idx = idx
 addPrefix ts idx =
   idx {
@@ -174,10 +176,10 @@
 index here fun var =
   case (here, fun', Numbered.toList var') of
     ([], [], []) ->
-      Nil
+      Empty
     ([], [(f, idx)], []) ->
       idx{minSize_ = succ (minSize_ idx),
-          prefix = buildList (con (Core.F f) `mappend` builder (prefix idx))}
+          prefix = buildList (con (unsafeMkSym f) `mappend` builder (prefix idx))}
     ([], [], [(x, idx)]) ->
       idx{minSize_ = succ (minSize_ idx),
           prefix = buildList (Term.var (V x) `mappend` builder (prefix idx))}
@@ -216,7 +218,7 @@
   where
     (!t, !v) = canonicalise (t0, v0) 
 
-    aux [] t Nil =
+    aux [] t Empty =
       leaf t (f v [])
 
     -- Non-empty prefix
@@ -233,18 +235,18 @@
     aux syms@(_:_) t idx =
       addPrefix (reverse syms) $ aux [] t idx
 
-    -- Empty prefix
-    aux [] Empty idx =
+    -- Nil prefix
+    aux [] Nil idx =
       index (f v (here idx)) (fun idx) (var idx)
     aux [] ConsSym{hd = App f _, rest = u} idx =
       index (here idx)
-        (update (fun_id f) idx' (fun idx))
+        (update (symId f) idx' (fun idx))
         (var idx)
       where
-        idx' = aux [] u (fun idx ! fun_id f)
+        idx' = aux [] u (fun idx ! symId f)
     aux [] ConsSym{hd = Var x, rest = u} idx =
       index (here idx) (fun idx)
-        (Numbered.modify (var_id x) Nil (aux [] u) (var idx))
+        (Numbered.modify (var_id x) Empty (aux [] u) (var idx))
 
 -- Helper for modify:
 -- Take an index with a prefix and pull out the first symbol of the prefix,
@@ -265,7 +267,7 @@
         minSize_ = size,
         prefix = Term.empty,
         here = [],
-        fun = Array.singleton (fun_id f) idx { prefix = ts, minSize_ = size - 1 },
+        fun = Array.singleton (symId f) idx { prefix = ts, minSize_ = size - 1 },
         var = Numbered.empty }
 
 -- | Look up a term in the index. Finds all key-value such that the search term
@@ -292,9 +294,13 @@
 matchesList t idx =
   run (search t emptyBindings idx Stop)
 
+-- | Check if a term is present in the index.
+member :: Term f -> Index f a -> Bool
+member t idx = not (Prelude.null (matches t idx))
+
 -- | Return all elements of the index.
 elems :: Index f a -> [a]
-elems Nil = []
+elems Empty = []
 elems idx =
   here idx ++
   concatMap elems (map snd (toList (fun idx))) ++
@@ -402,7 +408,7 @@
 search !_ !_ !_ _ | False = undefined
 search t binds idx rest =
   case idx of
-    Nil -> rest
+    Empty -> rest
     Index{..}
       | lenList t < minSize idx ->
         rest -- the search term is smaller than any in this index
@@ -442,7 +448,7 @@
           -- We've exhausted the prefix, so let's descend into the tree.
           -- Seems to work better to explore the function node first.
           case thd of
-            App f _ | idx@Index{} <- fun ! fun_id f ->
+            App f _ | idx@Index{} <- fun ! symId f ->
               -- Avoid creating a frame unnecessarily.
               case Numbered.size var of
                 0 -> search trest binds idx rest
@@ -453,7 +459,7 @@
                 _ -> searchVars thd ttl binds var 0 rest
     _ ->
       case prefix of
-        Empty ->
+        Nil ->
           -- The search term matches this node.
           case here of
             [] -> rest
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -22,7 +22,9 @@
     cfg_ground_join :: !Bool,
     cfg_use_connectedness_standalone :: !Bool,
     cfg_use_connectedness_in_ground_joining :: !Bool,
-    cfg_set_join :: !Bool }
+    cfg_set_join :: !Bool,
+    cfg_ground_join_limit :: !Int,
+    cfg_ground_join_incomplete_limit :: !Int }
 
 defaultConfig :: Config
 defaultConfig =
@@ -30,7 +32,9 @@
     cfg_ground_join = True,
     cfg_use_connectedness_standalone = True,
     cfg_use_connectedness_in_ground_joining = False,
-    cfg_set_join = False }
+    cfg_set_join = False,
+    cfg_ground_join_limit = maxBound,
+    cfg_ground_join_incomplete_limit = maxBound }
 
 {-# INLINEABLE joinCriticalPair #-}
 joinCriticalPair ::
@@ -58,9 +62,9 @@
           (normalForms (rewrite reduces (index_all idx)) (Map.singleton u []))) ->
       Right (Just cp, [])
     Just cp ->
-      case groundJoinFromMaybe config eqns idx mmodel (branches (And [])) cp of
-        Left model -> Left (cp, model)
-        Right (mcp, cps) -> Right (mcp, cps)
+      case groundJoinFromMaybe config 0 eqns idx mmodel (branches (And [])) cp of
+        (_, Left model) -> Left (cp, model)
+        (_, Right (mcp, cps)) -> Right (mcp, cps)
 
 {-# INLINEABLE step1 #-}
 {-# INLINEABLE step2 #-}
@@ -141,7 +145,8 @@
   (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Equation f -> Bool
 subsumed (eqns, complete) idx (t :=: u)
   | t == u = True
-  | otherwise = subsumed1 eqns idx (norm t :=: norm u)
+  | norm t == norm u = True
+  | otherwise = subsumed1 eqns idx (t :=: u)
   where
     norm t
       | Index.null complete = t
@@ -157,7 +162,7 @@
 subsumed1 eqns idx (App f ts :=: App g us)
   | f == g =
     let
-      sub Empty Empty = True
+      sub Nil Nil = True
       sub (Cons t ts) (Cons u us) =
         subsumed1 eqns idx (t :=: u) && sub ts us
       sub _ _ = error "Function used with multiple arities"
@@ -168,22 +173,25 @@
 {-# INLINEABLE groundJoin #-}
 groundJoin ::
   (Function f, Has a (Rule f)) =>
-  Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
-groundJoin config eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} =
+  Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))
+groundJoin config ticks _ _ _ cp
+  | ticks >= cfg_ground_join_incomplete_limit config =
+    (ticks, Right (Just cp, []))
+groundJoin config ticks eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} =
   case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of
     ([], instances) ->
       let cps = [ subst sub cp | sub <- instances ] in
-      Right (Just cp, usortBy (comparing (order . cp_eqn)) cps)
+      (ticks, Right (Just cp, usortBy (comparing (order . cp_eqn)) cps))
     (model:_, _) ->
-      groundJoinFrom config eqns idx model ctx cp
+      groundJoinFrom config (ticks+1) eqns idx model ctx cp
 
 {-# INLINEABLE groundJoinFrom #-}
 groundJoinFrom ::
   (Function f, Has a (Rule f)) =>
-  Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
-groundJoinFrom config@Config{..} eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}
-  | not cfg_ground_join = Left model
-  | modelOK model && isJust (allSteps config' eqns idx cp { cp_eqn = t' :=: u' }) = Left model
+  Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))
+groundJoinFrom config@Config{..} ticks eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}
+  | ticks >= cfg_ground_join_limit || not cfg_ground_join = (ticks, Left model)
+  | modelOK model && isJust (allSteps config' eqns idx cp { cp_eqn = t' :=: u' }) = (ticks, Left model)
   | otherwise =
       let
         model'
@@ -199,9 +207,9 @@
         weaken x = x
         ctx' = formAnd (diag (modelToLiterals model')) ctx in
 
-      case groundJoin config eqns idx ctx' cp of
-        Right (_, cps) | not (modelOK model) ->
-          Right (Nothing, cps)
+      case groundJoin config ticks eqns idx ctx' cp of
+        (ticks', Right (_, cps)) | not (modelOK model) ->
+          (ticks', Right (Nothing, cps))
         res -> res
   where
     config' = config{cfg_use_connectedness_standalone = False}
@@ -211,10 +219,23 @@
           normaliseWith (connectedIn m top) (rewrite (ok t u model) (index_all idx)) t
         _ -> normaliseWith (const True) (rewrite (ok t u m) (index_all idx)) t
     ok t u m rule sub =
-      reducesInModel m rule sub &&
-      unorient rule `simplerThan` (t :=: u)
+      case cp_top of
+        Just top | cfg_use_connectedness_in_ground_joining ->
+          reducesWith lessEqSkolemModel rule sub &&
+          unorient rule `simplerThan` (t :=: u)
+        _ ->
+          reducesInModel m rule sub &&
+          unorient rule `simplerThan` (t :=: u)
     connectedIn m top t =
       lessIn m t top == Just Strict
+    lessEqSkolemModel t u =
+      lessEqSkolem (subst reorderVars t) (subst reorderVars u)
+    reorderVars x =
+      var $
+      case modelVarValue model x of
+        Nothing -> V (var_id x + firstUnusedVar)
+        Just y -> y
+    firstUnusedVar = modelVarMaxBound model
 
     nt = normaliseIn model t u
     nu = normaliseIn model u t
@@ -230,9 +251,9 @@
 {-# INLINEABLE groundJoinFromMaybe #-}
 groundJoinFromMaybe ::
   (Function f, Has a (Rule f)) =>
-  Config -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) (Maybe (CriticalPair f), [CriticalPair f])
-groundJoinFromMaybe config eqns idx Nothing = groundJoin config eqns idx
-groundJoinFromMaybe config eqns idx (Just model) = groundJoinFrom config eqns idx model
+  Config -> Int -> (Index f (Equation f), Index f (Rule f)) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> (Int, Either (Model f) (Maybe (CriticalPair f), [CriticalPair f]))
+groundJoinFromMaybe config ticks eqns idx Nothing = groundJoin config ticks eqns idx
+groundJoinFromMaybe config ticks eqns idx (Just model) = groundJoinFrom config ticks eqns idx model
 
 {-# INLINEABLE valid #-}
 valid :: Function f => Model f -> Reduction f -> Bool
diff --git a/Twee/KBO.hs b/Twee/KBO.hs
--- a/Twee/KBO.hs
+++ b/Twee/KBO.hs
@@ -11,6 +11,7 @@
 import Data.Maybe
 import Control.Monad
 import Twee.Utils
+import Data.Intern
 
 lessEqSkolem :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
 lessEqSkolem !t !u
@@ -19,19 +20,19 @@
   where
     m = size t
     n = size u
-lessEqSkolem (App x Empty) _
+lessEqSkolem (App x Nil) _
   | x == minimal = True
-lessEqSkolem _ (App x Empty)
+lessEqSkolem _ (App x Nil)
   | x == minimal = False
 lessEqSkolem (Var x) (Var y) = x <= y
 lessEqSkolem (Var _) _ = True
 lessEqSkolem _ (Var _) = False
-lessEqSkolem (App (F _ f) ts) (App (F _ g) us) =
+lessEqSkolem (App (Sym f) ts) (App (Sym g) us) =
   case compare f g of
     LT -> True
     GT -> False
     EQ ->
-      let loop Empty Empty = True
+      let loop Nil Nil = True
           loop (Cons t ts) (Cons u us)
             | t == u = loop ts us
             | otherwise = lessEqSkolem t u
@@ -39,7 +40,7 @@
 
 -- | Check if one term is less than another in KBO.
 lessEq :: (Function f, Sized f, Weighted f) => Term f -> Term f -> Bool
-lessEq (App f Empty) _ | f == minimal = True
+lessEq (App f Nil) _ | f == minimal = True
 lessEq (Var x) (Var y) | x == y = True
 lessEq _ (Var _) = False
 lessEq (Var x) t = x `elem` vars t
@@ -49,7 +50,7 @@
    (st == su && f == g && lexLess ts us)) &&
   xs `lessVars` ys
   where
-    lexLess Empty Empty = True
+    lexLess Nil Nil = True
     lexLess (Cons t ts) (Cons u us)
       | t == u = lexLess ts us
       | otherwise =
@@ -57,7 +58,7 @@
         case unify t u of
           Nothing -> True
           Just sub
-            | not (allSubst (\_ (Cons t Empty) -> isMinimal t) sub) -> error "weird term inequality"
+            | not (allSubst (\_ (Cons t Nil) -> isMinimal t) sub) -> error "weird term inequality"
             | otherwise -> lexLess (subst sub ts) (subst sub us)
     lexLess _ _ = error "incorrect function arity"
     xs = weightedVars t
@@ -138,7 +139,7 @@
   | f << g = Just Strict
   | otherwise = Nothing
   where
-    loop Empty Empty = Just Nonstrict
+    loop Nil Nil = Just Nonstrict
     loop (Cons t ts) (Cons u us)
       | t == u = loop ts us
       | otherwise =
@@ -159,30 +160,30 @@
 class Weighted f where
   argWeight :: f -> Integer
 
-instance (Weighted f, Labelled f) => Weighted (Fun f) where
-  argWeight = argWeight . fun_value
+instance (Weighted f, Intern f) => Weighted (Sym f) where
+  argWeight = argWeight . unintern
 
-weightedVars :: (Weighted f, Labelled f) => Term f -> [(Var, Integer)]
+weightedVars :: (Weighted f, Intern f) => Term f -> [(Var, Integer)]
 weightedVars t = collate sum (loop 1 t)
   where
     loop k (Var x) = [(x, k)]
     loop k (App f ts) =
       concatMap (loop (k * argWeight f)) (unpack ts)
 
-instance (Labelled f, Sized f) => Sized (Fun f) where
-  size = size . fun_value
+instance (Intern f, Sized f) => Sized (Sym f) where
+  size = size . unintern
 
-instance (Labelled f, Sized f, Weighted f) => Sized (TermList f) where
+instance (Intern f, Sized f, Weighted f) => Sized (TermList f) where
   size = aux 0
     where
-      aux n Empty = n
+      aux n Nil = n
       aux n (Cons (App f t) u) =
         aux (n + size f + argWeight f * size t) u
       aux n (Cons (Var _) t) = aux (n+1) t
 
-instance (Labelled f, Sized f, Weighted f) => Sized (Term f) where
+instance (Intern f, Sized f, Weighted f) => Sized (Term f) where
   size = size . singleton
 
-instance (Labelled f, Sized f, Weighted f) => Sized (Equation f) where
+instance (Intern f, Sized f, Weighted f) => Sized (Equation f) where
   size (x :=: y) = size x + size y
 
diff --git a/Twee/Pretty.hs b/Twee/Pretty.hs
--- a/Twee/Pretty.hs
+++ b/Twee/Pretty.hs
@@ -11,6 +11,7 @@
 import Data.Set(Set)
 import Data.Ratio
 import Twee.Term
+import Data.Intern
 
 -- * Miscellaneous 'Pretty' instances and utilities.
 
@@ -69,13 +70,13 @@
 
 -- * Pretty-printing of terms.
 
-instance (Pretty f, Labelled f) => Pretty (Fun f) where
-  pPrintPrec l p = pPrintPrec l p . fun_value
+instance (Pretty f, Intern f) => Pretty (Sym f) where
+  pPrintPrec l p = pPrintPrec l p . unintern
 
-instance (Labelled f, PrettyTerm f) => Pretty (Term f) where
+instance (Intern f, PrettyTerm f) => Pretty (Term f) where
   pPrintPrec l p (Var x) = pPrintPrec l p x
   pPrintPrec l p (App f xs) =
-    pPrintTerm (termStyle (fun_value f)) l p (pPrint f) (unpack xs)
+    pPrintTerm (termStyle f) l p (pPrint f) (unpack xs)
 
 data HighlightedTerm f = HighlightedTerm [ANSICode] (Maybe [Int]) (Term f)
 
@@ -94,12 +95,12 @@
 maybeHighlight cs (Just []) d = highlight cs d
 maybeHighlight _ _ d = d
 
-instance (Labelled f, PrettyTerm f) => Pretty (HighlightedTerm f) where
+instance (Intern f, PrettyTerm f) => Pretty (HighlightedTerm f) where
   pPrintPrec l p (HighlightedTerm cs h (Var x)) =
     maybeHighlight cs h (pPrintPrec l p x)
   pPrintPrec l p (HighlightedTerm cs h (App f xs)) =
     maybeHighlight cs h $
-    pPrintTerm (termStyle (fun_value f)) l p (pPrint f)
+    pPrintTerm (termStyle f) l p (pPrint f)
       (zipWith annotate [0..] (unpack xs))
     where
       annotate i t =
@@ -107,10 +108,10 @@
           Just (n:ns) | i == n -> HighlightedTerm cs (Just ns) t
           _ -> HighlightedTerm cs Nothing t
 
-instance (Labelled f, PrettyTerm f) => Pretty (TermList f) where
+instance (Intern f, PrettyTerm f) => Pretty (TermList f) where
   pPrintPrec _ _ = pPrint . unpack
 
-instance (Labelled f, PrettyTerm f) => Pretty (Subst f) where
+instance (Intern f, PrettyTerm f) => Pretty (Subst f) where
   pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"
     where
       docs =
@@ -122,6 +123,9 @@
   -- | The style of the function symbol. Defaults to 'curried'.
   termStyle :: f -> TermStyle
   termStyle _ = curried
+
+instance (Intern f, PrettyTerm f) => PrettyTerm (Sym f) where
+  termStyle = termStyle . unintern
 
 -- | Defines how to print out a function symbol.
 newtype TermStyle =
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -8,7 +8,7 @@
   lemma, autoSubst, simpleLemma, axiom, symm, trans, cong, congPath,
 
   -- * Analysing proofs
-  simplify, steps, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,
+  simplify, steps, stepTerms, usedLemmas, usedAxioms, usedLemmasAndSubsts, usedAxiomsAndSubsts,
   groundAxiomsAndSubsts, eliminateDefinitions, eliminateDefinitionsFromGoal,
   simplifyProof, generaliseProof,
 
@@ -64,7 +64,7 @@
     -- | Congruence.
     -- Parallel, i.e., takes a function symbol and one derivation for each
     -- argument of that function.
-  | Cong {-# UNPACK #-} !(Fun f) ![Derivation f]
+  | Cong {-# UNPACK #-} !(Sym f) ![Derivation f]
   deriving (Eq, Show)
 
 --  | An axiom, which comes without proof.
@@ -148,7 +148,7 @@
 
 instance Function f => Pretty (Proof f) where
   pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation)
-instance (Labelled f, PrettyTerm f) => Pretty (Derivation f) where
+instance (Intern f, PrettyTerm f) => Pretty (Derivation f) where
   pPrint (UseLemma lemma sub) =
     text "subst" <#> pPrintTuple [text "lemma" <+> pPrint (equation lemma), pPrint sub]
   pPrint (UseAxiom axiom sub) =
@@ -162,12 +162,12 @@
   pPrint (Cong f ps) =
     text "cong" <#> pPrintTuple (pPrint f:map pPrint ps)
 
-instance (Labelled f, PrettyTerm f) => Pretty (Axiom f) where
+instance (Intern f, PrettyTerm f) => Pretty (Axiom f) where
   pPrint Axiom{..} =
     text "axiom" <#>
     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
 
-foldLemmas :: (Labelled f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
+foldLemmas :: (Intern f, PrettyTerm f) => (Map (Proof f) a -> Derivation f -> a) -> [Derivation f] -> Map (Proof f) a
 foldLemmas op ds =
   execState (mapM_ foldGoal ds) Map.empty
   where
@@ -247,7 +247,7 @@
   Trans p (trans q r)
 trans p q = Trans p q
 
-cong :: Fun f -> [Derivation f] -> Derivation f
+cong :: Sym f -> [Derivation f] -> Derivation f
 cong f ps =
   case sequence (map unRefl ps) of
     Nothing -> Cong f ps
@@ -312,6 +312,28 @@
 fromSteps (t :=: _) [] = Refl t
 fromSteps _ ps = foldr1 Trans ps
 
+-- | Given a derivation, compute which terms it goes through.
+stepTerms :: Function f => Derivation f -> [Term f]
+stepTerms p =
+  case steps p of
+    [] -> [eqn_lhs (equation (certify p))]
+    s:ss ->
+      eqn_lhs (equation (certify s)):
+      map (eqn_rhs . equation . certify) (s:ss)
+
+-- | Find peak terms in a derivation.
+peakTerms :: Function f => Derivation f -> [Term f]
+peakTerms = peaks . stepTerms
+  where
+    peaks [] = []
+    peaks [t] = [t]
+    peaks (t:u:ts)
+      | lessEq t u = peaks (u:ts)
+      | lessEq u t = peaks (t:ts)
+      | otherwise = t:peaks (u:ts)
+      -- TODO do more carefully?
+      -- handle this case t --> v <-- u where e.g. t <= u (should still be counted as a peak perhaps)
+
 -- | Find all lemmas which are used in a derivation.
 usedLemmas :: Derivation f -> [Proof f]
 usedLemmas p = map fst (usedLemmasAndSubsts p)
@@ -383,7 +405,7 @@
       case find (build (app f (map var vs))) of
         Nothing -> Cong f (map elim ps)
         Just (rhs, Subst sub) ->
-          let proof (Cons (Var (V x)) Empty) = qs !! x in
+          let proof (Cons (Var (V x)) Nil) = qs !! x in
           replace (proof <$> sub) rhs
       where
         vs = map V [0..length ps-1]
@@ -391,7 +413,7 @@
 
     elimSubst (Subst sub) = Subst (singleton <$> term <$> unsingleton <$> sub)
       where
-        unsingleton (Cons t Empty) = t
+        unsingleton (Cons t Nil) = t
 
     term = build . term'
     term' (Var x) = var x
@@ -445,7 +467,13 @@
     -- | Print out proofs in colour.
     cfg_use_colour :: !Bool,
     -- | Print out which instances of some axioms were used.
-    cfg_show_uses_of_axioms :: Axiom f -> Bool }
+    cfg_show_uses_of_axioms :: Axiom f -> Bool,
+    -- | Print out peaks of each lemma.
+    cfg_show_peaks :: !Bool,
+    -- | Eliminate $equals from the proofs.
+    cfg_eliminate_existentials_coding :: !Bool,
+    -- | Show which subterm is rewritten.
+    cfg_show_subterms :: !Bool }
 
 -- | The default configuration.
 defaultConfig :: Config f
@@ -456,7 +484,10 @@
     cfg_ground_proof = False,
     cfg_show_instances = False,
     cfg_use_colour = False,
-    cfg_show_uses_of_axioms = const False }
+    cfg_show_uses_of_axioms = const False,
+    cfg_show_peaks = False,
+    cfg_eliminate_existentials_coding = True,
+    cfg_show_subterms = False }
 
 -- | A proof, with all axioms and lemmas explicitly listed.
 data Presentation f =
@@ -514,8 +545,8 @@
   pPrint = pPrintPresentation defaultConfig
 
 -- | Simplify and present a proof.
-present :: Function f => Config f -> [ProvedGoal f] -> Presentation f
-present config@Config{..} goals =
+present :: Function f => Config f -> [Proof f] -> [ProvedGoal f] -> Presentation f
+present config@Config{..} extraLemmas goals =
   Presentation axioms lemmas goals'
   where
     ps =
@@ -523,14 +554,14 @@
       simplifyProof config $ map (derivation . pg_proof) goals
 
     goals' =
-      [ decodeGoal (goal{pg_proof = certify p})
+      [ decodeGoal config (goal{pg_proof = certify p})
       | (goal, p) <- zip goals ps ]
 
     axioms = usort $
       concatMap (usedAxioms . derivation . pg_proof) goals' ++
       concatMap (usedAxioms . derivation) lemmas
 
-    lemmas = allLemmas (map (derivation . pg_proof) goals')
+    lemmas = allLemmas (map simpleLemma extraLemmas ++ map (derivation . pg_proof) goals')
 
 groundProof :: Function f => [Derivation f] -> [Derivation f]
 groundProof ds
@@ -598,9 +629,10 @@
     shouldInline p =
       cfg_no_lemmas ||
       length (filter (not . invisible) (map (equation . certify) (steps (derivation p)))) <= 1 ||
-      (not cfg_all_lemmas &&
-       (isJust (decodeEquality (eqn_lhs (equation p))) ||
-        isJust (decodeEquality (eqn_rhs (equation p)))))
+      (cfg_eliminate_existentials_coding &&
+        (any (isJust . decodeEquality) [eqn_lhs (equation p), eqn_rhs (equation p)] ||
+         any isFalseTerm [eqn_lhs (equation p), eqn_rhs (equation p)] ||
+         any isTrueTerm [eqn_lhs (equation p), eqn_rhs (equation p)]))
 
     subsuming lem (t :=: u) =
       subsuming1 lem (t :=: u) ++
@@ -742,16 +774,22 @@
 pPrintLemma Config{..} axiomNum lemmaNum p
   | null qs = text "Reflexivity."
   | equation (certify (fromSteps (equation p) qs)) == equation p =
-    vcat (zipWith pp hl qs) $$ ppTerm (eqn_rhs (equation p))
+    vcat (zipWith pp hl qs) $$ ppTerm (HighlightedTerm [] Nothing) (eqn_rhs (equation p))
   | otherwise = error "lemma changed by pretty-printing!"
   where
     qs = steps (derivation p)
     hl = map highlightStep qs
+    peaks = Set.fromList (peakTerms (derivation p))
 
     pp _ p | invisible (equation (certify p)) = pPrintEmpty
     pp h p =
-      ppTerm (HighlightedTerm [green | cfg_use_colour] (Just h) (eqn_lhs (equation (certify p)))) $$
-      text "=" <+> highlight [bold | cfg_use_colour] (text "{ by" <+> ppStep p <+> text "}")
+      ppTerm (HighlightedTerm [green | cfg_use_colour] (Just h)) (eqn_lhs (equation (certify p))) $$
+      text "=" <+> highlight [bold | cfg_use_colour] (text "{" <+> ((text "by" <+> ppStep p) $$ if cfg_show_subterms then subtermInfo else pPrintEmpty) <+> text "}")
+      where
+        subtermInfo =
+          (text "from" <+> pPrint t) $$
+          (text "to" <+> pPrint u)
+        t :=: u = rewrittenSubterms p
 
     highlightStep UseAxiom{} = []
     highlightStep UseLemma{} = []
@@ -760,8 +798,16 @@
       where
         [(i, p)] = filter (not . isRefl . snd) (zip [0..] ps)
 
-    ppTerm t = text "  " <#> pPrint t
+    rewrittenSubterms (Symm p) = u :=: t
+      where
+        t :=: u = rewrittenSubterms p
+    rewrittenSubterms (Cong _ ps) = rewrittenSubterms p
+      where
+        [p] = filter (not . isRefl) ps
+    rewrittenSubterms p = equation (certify p)
 
+    ppTerm decorate t = text "  " <#> pPrint (decorate t) <+> (if cfg_show_peaks && t `Set.member` peaks then text "(peak)" else pPrintEmpty)
+
     ppStep = pp True
       where
         pp dir (UseAxiom axiom@Axiom{..} sub) =
@@ -826,7 +872,7 @@
               [ pPrint x <+> text "=" <+> pPrint t
               | (x, t) <- substToList sub ],
             if minimal `elem` funs sub then
-              text "where" <+> doubleQuotes (pPrint (minimal :: Fun f)) <+>
+              text "where" <+> doubleQuotes (pPrint (minimal :: Sym f)) <+>
               text "stands for an arbitrary term of your choice."
             else pPrintEmpty,
             text ""]
@@ -895,9 +941,9 @@
 
 -- Tries to transform a proof of $true = $false into a proof of
 -- the original existentially-quantified formula.
-decodeGoal :: Function f => ProvedGoal f -> ProvedGoal f
-decodeGoal pg =
-  case maybeDecodeGoal pg of
+decodeGoal :: Function f => Config f -> ProvedGoal f -> ProvedGoal f
+decodeGoal config pg =
+  case maybeDecodeGoal config pg of
     Nothing -> pg
     Just (name, witness, goal, deriv) ->
       checkProvedGoal $
@@ -908,8 +954,9 @@
         pg_witness_hint = witness }
 
 maybeDecodeGoal :: forall f. Function f =>
-  ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
-maybeDecodeGoal ProvedGoal{..}
+  Config f -> ProvedGoal f -> Maybe (String, Subst f, Equation f, Derivation f)
+maybeDecodeGoal Config{..} ProvedGoal{..}
+  | not cfg_eliminate_existentials_coding = Nothing
   --  N.B. presentWithGoals takes care of expanding any lemma which mentions
   --  $equals, and flattening the proof.
   | isFalseTerm u = extract (steps deriv)
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -84,7 +84,7 @@
     -- 
     -- A rule with orientation @'WeaklyOriented' k ts@ can be used unless
     -- all terms in @ts@ are equal to @k@.
-  | WeaklyOriented {-# UNPACK #-} !(Fun f) [Term f]
+  | WeaklyOriented {-# UNPACK #-} !(Sym f) [Term f]
     -- | A permutative rule.
     --
     -- A rule with orientation @'Permutative' ts@ can be used if
@@ -124,7 +124,7 @@
   subst_ sub (Permutative ts) = Permutative (subst_ sub ts)
   subst_ _   Unoriented = Unoriented
 
-instance (Labelled f, PrettyTerm f) => Pretty (Rule f) where
+instance (Intern f, PrettyTerm f) => Pretty (Rule f) where
   pPrint (Rule or _ l r) =
     pPrint l <+> text (showOrientation or) <+> pPrint r
     where
@@ -149,7 +149,7 @@
         case unify t u of
           Nothing -> Oriented
           Just sub
-            | allSubst (\_ (Cons t Empty) -> isMinimal t) sub ->
+            | allSubst (\_ (Cons t Nil) -> isMinimal t) sub ->
               WeaklyOriented minimal (map (build . var . fst) (substToList sub))
             | otherwise -> Unoriented
       | lessEq t u = error "wrongly-oriented rule"
@@ -212,7 +212,7 @@
   where
     u = build (simp (singleton t))
 
-    simp Empty = mempty
+    simp Nil = mempty
     simp (Cons (Var x) t) = var x `mappend` simp t
     simp (Cons t u)
       | Just (rule, sub) <- simpleRewrite idx t =
@@ -385,7 +385,7 @@
     expand t@(Var x) = fromMaybe t (Term.lookup x sub)
     expand t = t
 
-    isMinimal (App f Empty) = f == min
+    isMinimal (App f Nil) = f == min
     isMinimal _ = False
 reducesWith p (Rule (Permutative ts) _ _ _) sub =
   aux ts
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -1,7 +1,7 @@
 -- | Terms and substitutions.
 --
 -- Terms in twee are represented as arrays rather than as an algebraic data
--- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Empty')
+-- type. This module defines pattern synonyms ('App', 'Var', 'Cons', 'Nil')
 -- which means that pattern matching on terms works just as normal.
 -- The pattern synonyms can not be used to create new terms; for that you
 -- have to use a builder interface ('Build').
@@ -20,26 +20,24 @@
 #endif
 module Twee.Term(
   -- * Terms
-  Term, pattern Var, pattern App, isApp, isVar, singleton, len,
+  Term, Var(..), pattern Var, pattern App, isApp, isVar, singleton, len,
   -- * Termlists
-  TermList, pattern Empty, pattern Cons, pattern ConsSym, hd, tl, rest,
+  TermList, pattern Nil, pattern Cons, pattern ConsSym, hd, tl, rest,
   pattern UnsafeCons, pattern UnsafeConsSym, uhd, utl, urest,
   empty, unpack, lenList,
-  -- * Function symbols and variables
-  Fun, fun, fun_id, fun_value, pattern F, Var(..), Labelled(..),
   -- * Building terms
   Build(..),
   Builder,
   build, buildList,
   con, app, var,
   -- * Access to subterms
-  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath,
+  children, properSubterms, subtermsList, subterms, reverseSubtermsList, reverseSubterms, occurs, isSubtermOf, isSubtermOfList, at, listAt, atPath, listDrop,
   -- * Substitutions
   Substitution(..),
   subst,
   Subst(..),
   -- ** Constructing and querying substitutions
-  emptySubst, listToSubst, substToList,
+  emptySubst, listToSubst, substToList, substToList',
   lookup, lookupList,
   extend, extendList, unsafeExtendList,
   retract,
@@ -77,8 +75,7 @@
 import qualified Data.IntMap.Strict as IntMap
 import Control.Arrow((&&&))
 import Twee.Utils
-import qualified Data.Label as Label
-import Data.Typeable
+import Data.Intern
 import GHC.Stack
 
 --------------------------------------------------------------------------------
@@ -116,21 +113,21 @@
 build :: Build a => a -> Term (BuildFun a)
 build x =
   case buildList x of
-    Cons t Empty -> t
+    Cons t Nil -> t
 
 -- | Build a termlist.
 {-# INLINE buildList #-}
 buildList :: Build a => a -> TermList (BuildFun a)
-buildList x = buildTermList (builder x)
+buildList x = buildTermList 16 (builder x)
 
 -- | Build a constant (a function with no arguments).
 {-# INLINE con #-}
-con :: Fun f -> Builder f
+con :: Sym f -> Builder f
 con x = emitApp x mempty
 
 -- | Build a function application.
 {-# INLINE app #-}
-app :: Build a => Fun (BuildFun a) -> a -> Builder (BuildFun a)
+app :: Build a => Sym (BuildFun a) -> a -> Builder (BuildFun a)
 app f ts = emitApp f (builder ts)
 
 -- | Build a variable.
@@ -149,7 +146,7 @@
 {-# INLINE substToList #-}
 substToList :: Subst f -> [(Var, Term f)]
 substToList sub =
-  [(x, t) | (x, Cons t Empty) <- substToList' sub]
+  [(x, t) | (x, Cons t Nil) <- substToList' sub]
 
 -- | Fold a function over a substitution.
 {-# INLINE foldSubst #-}
@@ -185,7 +182,7 @@
   substList :: s -> TermList (SubstFun s) -> Builder (SubstFun s)
   substList sub ts = aux ts
     where
-      aux Empty = mempty
+      aux Nil = mempty
       aux (Cons (Var x) ts) = evalSubst sub x <> aux ts
       aux (Cons (App f ts) us) = app f (aux ts) <> aux us
 
@@ -277,7 +274,7 @@
 idempotentOn :: Subst f -> TermList f -> Bool
 idempotentOn !sub = aux
   where
-    aux Empty = True
+    aux Nil = True
     aux ConsSym{hd = App{}, rest = t} = aux t
     aux (Cons (Var x) t) = isNothing (lookupList x sub) && aux t
 
@@ -298,15 +295,15 @@
   where
     (V m, V n) = boundLists (t:ts)
     vars =
-      buildTermList $
+      buildTermList (n-m+2) $
         -- Produces two variables when the term is ground
         -- (n = minBound, m = maxBound), which is OK.
         mconcat [emitVar (V x) | x <- [0..n-m+1]]
 
     loop !_ !_ !_ !_ | never = undefined
-    loop sub _ Empty [] = sub
-    loop sub Empty _ _ = sub
-    loop sub vs Empty (t:ts) = loop sub vs t ts
+    loop sub _ Nil [] = sub
+    loop sub Nil _ _ = sub
+    loop sub vs Nil (t:ts) = loop sub vs t ts
     loop sub vs ConsSym{hd = App{}, rest = t} ts = loop sub vs t ts
     loop sub vs0@(Cons v vs) (Cons (Var x) t) ts =
       case extend x v sub of
@@ -364,7 +361,7 @@
               sub <- extend x t sub
               loop sub pats ts
             _ -> Nothing
-        loop sub _ Empty = Just sub
+        loop sub _ Nil = Just sub
         loop _ _ _ = Nothing
     in loop sub pat t
 
@@ -416,7 +413,7 @@
   {-# INLINE substList #-}
   substList (Triangle sub) ts = aux ts
     where
-      aux Empty = mempty
+      aux Nil = mempty
       aux (Cons (Var x) ts) = auxVar x <> aux ts
       aux (Cons (App f ts) us) = app f (aux ts) <> aux us
 
@@ -480,7 +477,7 @@
           sub <- var sub x t
           loop sub ts us
         _ -> Nothing
-    loop sub _ Empty = Just sub
+    loop sub _ Nil = Just sub
     loop _ _ _ = Nothing
 
     {-# INLINE var #-}
@@ -539,18 +536,18 @@
 unpack :: TermList f -> [Term f]
 unpack t = unfoldr op t
   where
-    op Empty = Nothing
+    op Nil = Nothing
     op (Cons t ts) = Just (t, ts)
 
-instance (Labelled f, Show f) => Show (Term f) where
+instance (Intern f, Show f) => Show (Term f) where
   show (Var x) = show x
-  show (App f Empty) = show f
+  show (App f Nil) = show f
   show (App f ts) = show f ++ "(" ++ intercalate "," (map show (unpack ts)) ++ ")"
 
-instance (Labelled f, Show f) => Show (TermList f) where
+instance (Intern f, Show f) => Show (TermList f) where
   show = show . unpack
 
-instance (Labelled f, Show f) => Show (Subst f) where
+instance (Intern f, Show f) => Show (Subst f) where
   show subst =
     show
       [ (i, t)
@@ -561,7 +558,7 @@
 {-# INLINE lookup #-}
 lookup :: Var -> Subst f -> Maybe (Term f)
 lookup x s = do
-  Cons t Empty <- lookupList x s
+  Cons t Nil <- lookupList x s
   return t
 
 -- | Add a new binding to a substitution.
@@ -604,7 +601,7 @@
 subtermsList :: TermList f -> [Term f]
 subtermsList t = unfoldr op t
   where
-    op Empty = Nothing
+    op Nil = Nothing
     op ConsSym{hd = t, rest = u} = Just (t, u)
 
 -- | Find all subterms of a term.
@@ -652,20 +649,20 @@
 t `isSubtermOf` u = t `isSubtermOfList` singleton u
 
 -- | Map a function over the function symbols in a term.
-mapFun :: (Fun f -> Fun g) -> Term f -> Builder g
+mapFun :: (Sym f -> Sym g) -> Term f -> Builder g
 mapFun f = mapFunList f . singleton
 
 -- | Map a function over the function symbols in a termlist.
-mapFunList :: (Fun f -> Fun g) -> TermList f -> Builder g
+mapFunList :: (Sym f -> Sym g) -> TermList f -> Builder g
 mapFunList f ts = aux ts
   where
-    aux Empty = mempty
+    aux Nil = mempty
     aux (Cons (Var x) ts) = var x `mappend` aux ts
     aux (Cons (App ff ts) us) = app (f ff) (aux ts) `mappend` aux us
 
 {-# INLINE replace #-}
 replace :: (Build a, BuildFun a ~ f) => Term f -> a -> TermList f -> Builder f
-replace !_ !_ Empty = mempty
+replace !_ !_ Nil = mempty
 replace t u (Cons v vs)
   | t == v = builder u `mappend` replace t u vs
   | len v < len t = builder v `mappend` replace t u vs
@@ -680,7 +677,7 @@
 replacePosition n !x = aux n
   where
     aux !_ !_ | never = undefined
-    aux _ Empty = mempty
+    aux _ Nil = mempty
     aux 0 (Cons _ t) = builder x `mappend` builder t
     aux n (Cons (Var x) t) = var x `mappend` aux (n-1) t
     aux n (Cons t@(App f ts) u)
@@ -696,7 +693,7 @@
 replacePositionSub sub n !x = aux n
   where
     aux !_ !_ | never = undefined
-    aux _ Empty = mempty
+    aux _ Nil = mempty
     aux n (Cons t u)
       | n < len t = inside n t `mappend` outside u
       | otherwise = outside (singleton t) `mappend` aux (n-len t) u
@@ -714,7 +711,7 @@
     term _ 0 = []
     term t n = list 0 (children t) (n-1)
 
-    list _ Empty _ = error "bad position"
+    list _ Nil _ = error "bad position"
     list k (Cons t u) n
       | n < len t = k:term t n
       | otherwise = list (k+1) u (n-len t)
@@ -726,33 +723,11 @@
     term k _ [] = k
     term k t (n:ns) = list (k+1) (children t) n ns
 
-    list _ Empty _ _ = error "bad path"
+    list _ Nil _ _ = error "bad path"
     list k (Cons t _) 0 ns = term k t ns
     list k (Cons t u) n ns =
       list (k+len t) u (n-1) ns
 
-class Labelled f where
-  label :: f -> Label.Label f
-  default label :: (Ord f, Typeable f) => f -> Label.Label f
-  label = Label.label
-
-instance (Labelled f, Show f) => Show (Fun f) where show = show . fun_value
-
--- | A pattern which extracts the 'fun_value' from a 'Fun'.
-pattern F :: Labelled f => Int -> f -> Fun f
-pattern F x y <- (fun_id &&& fun_value -> (x, y))
-{-# COMPLETE F #-}
-
--- | Compare the 'fun_value's of two 'Fun's.
-(<<) :: (Labelled f, Ord f) => Fun f -> Fun f -> Bool
-f << g = fun_value f < fun_value g
-
--- | Construct a 'Fun' from a function symbol.
-{-# NOINLINE fun #-}
-fun :: Labelled f => f -> Fun f
-fun f = Core.F (fromIntegral (Label.labelNum (label f)))
-
--- | The underlying function symbol of a 'Fun'.
-{-# INLINE fun_value #-}
-fun_value :: Labelled f => Fun f -> f
-fun_value x = Label.find (Label.unsafeMkLabel (fromIntegral (fun_id x)))
+-- | Compare the values of two 'Sym's.
+(<<) :: (Intern f, Ord f) => Sym f -> Sym f -> Bool
+f << g = unintern f < unintern g
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -25,6 +25,7 @@
 import GHC.ST hiding (liftST)
 import Data.Ord
 import Twee.Profile
+import Data.Intern
 
 --------------------------------------------------------------------------------
 -- Symbols. A symbol is a single function or variable in a flatterm.
@@ -72,7 +73,7 @@
 --------------------------------------------------------------------------------
 
 -- | @'TermList' f@ is a list of terms whose function symbols have type @f@.
--- It is either a 'Cons' or an 'Empty'. You can turn it into a @['Term' f]@
+-- It is either a 'Cons' or an 'Nil'. You can turn it into a @['Term' f]@
 -- with 'Twee.Term.unpack'.
 
 -- A TermList is a slice of an unboxed array of symbols.
@@ -90,12 +91,22 @@
   | n < 0 || low t + n >= high t = error "term index out of bounds"
   | otherwise = t `unsafeListAt` n
 
+-- | Get a suffix of a termlist.
+listDrop :: TermList f -> Int -> TermList f
+t `listDrop` n
+  | n < 0 || low t + n > high t = error "term index out of bounds"
+  | otherwise = t `unsafeListDrop` n
+
 -- | Index into a termlist, without bounds checking.
 unsafeListAt :: TermList f -> Int -> Term f
 TermList lo hi arr `unsafeListAt` n =
   case TermList (lo+n) hi arr of
     UnsafeCons t _ -> t
 
+-- | Get a suffix of a termlist, without bounds checking.
+unsafeListDrop :: TermList f -> Int -> TermList f
+TermList lo hi arr `unsafeListDrop` n = TermList (lo+n) hi arr
+
 {-# INLINE lenList #-}
 -- | The length of (number of symbols in) a termlist.
 lenList :: TermList f -> Int
@@ -120,8 +131,8 @@
   compare = comparing termlist
 
 -- Pattern synonyms for termlists:
--- * Empty :: TermList f
---   Empty is the empty termlist.
+-- * Nil :: TermList f
+--   Nil is the empty termlist.
 -- * Cons t ts :: Term f -> TermList f -> TermList f
 --   Cons t ts is the termlist t:ts.
 -- * ConsSym t ts :: Term f -> TermList f -> TermList f
@@ -131,15 +142,15 @@
 --   that the termlist is non-empty.
 
 -- | Matches the empty termlist.
-pattern Empty :: TermList f
-pattern Empty <- (patHead -> Nothing)
+pattern Nil :: TermList f
+pattern Nil <- (patHead -> Nothing)
 
 -- | Matches a non-empty termlist, unpacking it into head and tail.
 pattern Cons :: Term f -> TermList f -> TermList f
 pattern Cons t ts <- (patHead -> Just (t, _, ts))
 
-{-# COMPLETE Empty, Cons #-}
-{-# COMPLETE Empty, ConsSym #-}
+{-# COMPLETE Nil, Cons #-}
+{-# COMPLETE Nil, ConsSym #-}
 
 -- | Like 'Cons', but does not check that the termlist is non-empty. Use only if
 -- you are sure the termlist is non-empty.
@@ -183,17 +194,7 @@
 
 -- Pattern synonyms for single terms.
 -- * Var :: Var -> Term f
--- * App :: Fun f -> TermList f -> Term f
-
--- | A function symbol. @f@ is the underlying type of function symbols defined
--- by the user; @'Fun' f@ is an @f@ together with an automatically-generated unique number.
-newtype Fun f =
-  F {
-    -- | The unique number of a 'Fun'. Must fit in 32 bits.
-    fun_id :: Int }
-  deriving (Eq, Ord)
-
-type role Fun nominal
+-- * App :: Sym f -> TermList f -> Term f
 
 -- | A variable.
 newtype Var =
@@ -210,16 +211,16 @@
 pattern Var x <- (patTerm -> Left x)
 
 -- | Matches a function application.
-pattern App :: Fun f -> TermList f -> Term f
+pattern App :: Sym f -> TermList f -> Term f
 pattern App f ts <- (patTerm -> Right (f, ts))
 
 {-# COMPLETE Var, App #-}
 
 -- A helper function for Var and App.
 {-# INLINE patTerm #-}
-patTerm :: Term f -> Either Var (Fun f, TermList f)
+patTerm :: Term f -> Either Var (Sym f, TermList f)
 patTerm Term{..}
-  | isFun     = Right (F index, ts)
+  | isFun     = Right (unsafeMkSym index, ts)
   | otherwise = Left (V index)
   where
     Symbol{..} = toSymbol root
@@ -277,11 +278,10 @@
 
 -- Build a termlist from a Builder.
 {-# INLINE buildTermList #-}
-buildTermList :: Builder f -> TermList f
-buildTermList (Builder m) = stamp "build term" $ runST $ do
+buildTermList :: Int -> Builder f -> TermList f
+buildTermList initialSize (Builder m) = stamp "build term" $ runST $ do
   MutableByteArray marr# <-
-    -- Start with a capacity of 16 symbols (arbitrary choice)
-    newByteArray (16 * symbolSize)
+    newByteArray (max 1 initialSize * symbolSize)
   (marr, n) <-
     ST $ \s ->
       case m s marr# 0# of
@@ -326,8 +326,8 @@
 
 -- Emit a function application.
 {-# INLINE emitApp #-}
-emitApp :: Fun f -> Builder f -> Builder f
-emitApp (F n) inner = emitSymbolBuilder (Symbol True n 0) inner
+emitApp :: Sym f -> Builder f -> Builder f
+emitApp f inner = emitSymbolBuilder (Symbol True (symId f) 0) inner
 
 -- Emit a variable.
 {-# INLINE emitVar #-}
@@ -394,5 +394,5 @@
 occursList (V x) t = symbolOccursList (fromSymbol (Symbol False x 1)) t
 
 symbolOccursList :: Int64 -> TermList f -> Bool
-symbolOccursList !_ Empty = False
+symbolOccursList !_ Nil = False
 symbolOccursList n ConsSym{hd = t, rest = ts} = root t == n || symbolOccursList n ts
diff --git a/twee-lib.cabal b/twee-lib.cabal
--- a/twee-lib.cabal
+++ b/twee-lib.cabal
@@ -1,5 +1,5 @@
 name:                twee-lib
-version:             2.5
+version:             2.6.1
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -26,7 +26,7 @@
 
 source-repository head
   type:     git
-  location: git://github.com/nick8325/twee.git
+  location: https://github.com/nick8325/twee.git
   branch:   master
 
 flag llvm
@@ -64,7 +64,7 @@
     Twee.Task
     Twee.Utils
     Twee.Term.Core
-    Data.Label
+    Data.Intern
   other-modules:
     Data.BatchedQueue
     Data.ChurchList
@@ -88,8 +88,9 @@
     cereal,
     QuickCheck
   hs-source-dirs:      .
-  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports
+  ghc-options:         -W -fno-warn-incomplete-patterns -fno-warn-dodgy-imports -fno-warn-x-partial
   default-language:    Haskell2010
+  default-extensions:  TypeOperators
 
   if flag(llvm)
     cpp-options: -DUSE_LLVM