diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -7,7 +7,7 @@
 import qualified Twee.Rule as Rule
 import Twee.Equation
 import qualified Twee.Proof as Proof
-import Twee.Proof(Proof, Axiom(..), Lemma(..), ProvedGoal(..), provedGoal, certify, derivation, symm)
+import Twee.Proof(Axiom(..), Proof(..), ProvedGoal(..), provedGoal, certify, derivation, symm)
 import Twee.CP hiding (Config)
 import qualified Twee.CP as CP
 import Twee.Join hiding (Config, defaultConfig)
@@ -300,7 +300,6 @@
 instance Has (ActiveRule f) Depth where the = rule_depth
 instance f ~ g => Has (ActiveRule f) (Rule g) where the = rule_rule
 instance f ~ g => Has (ActiveRule f) (Proof g) where the = rule_proof
-instance f ~ g => Has (ActiveRule f) (Lemma g) where the x = Lemma (the x) (the x)
 instance f ~ g => Has (ActiveRule f) (Positions g) where the = rule_positions
 
 newtype RuleId = RuleId Id deriving (Eq, Ord, Show, Num, Real, Integral, Enum)
diff --git a/Twee/CP.hs b/Twee/CP.hs
--- a/Twee/CP.hs
+++ b/Twee/CP.hs
@@ -14,7 +14,7 @@
 import Twee.Utils
 import Twee.Equation
 import qualified Twee.Proof as Proof
-import Twee.Proof(Derivation, Lemma, congPath)
+import Twee.Proof(Derivation, Proof, congPath)
 
 -- | The set of positions at which a term can have critical overlaps.
 data Positions f = NilP | ConsP {-# UNPACK #-} !Int !(Positions f)
@@ -300,7 +300,7 @@
 -- | Make a critical pair from two rules and an overlap.
 {-# INLINEABLE makeCriticalPair #-}
 makeCriticalPair ::
-  (Has a (Rule f), Has a (Lemma f), Has a Id, Function f) =>
+  (Has a (Rule f), Has a (Proof f), Has a Id, Function f) =>
   a -> a -> Overlap f -> Maybe (CriticalPair f)
 makeCriticalPair r1 r2 overlap@Overlap{..}
   | lessEq overlap_top t = Nothing
@@ -318,7 +318,7 @@
 {-# INLINEABLE overlapProof #-}
 overlapProof ::
   forall a f.
-  (Has a (Rule f), Has a (Lemma f), Has a Id) =>
+  (Has a (Rule f), Has a (Proof f), Has a Id) =>
   a -> a -> Overlap f -> Derivation f
 overlapProof left right Overlap{..} =
   Proof.symm (reductionProof (step left leftSub))
diff --git a/Twee/Index.hs b/Twee/Index.hs
--- a/Twee/Index.hs
+++ b/Twee/Index.hs
@@ -5,9 +5,13 @@
 -- the search term is an instance of the key, and return the corresponding
 -- values.
 
-{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts #-}
+{-# LANGUAGE BangPatterns, RecordWildCards, OverloadedStrings, FlexibleContexts, CPP #-}
 -- We get some bogus warnings because of pattern synonyms.
 {-# OPTIONS_GHC -fno-warn-overlapping-patterns #-}
+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
+#ifdef USE_LLVM
+{-# OPTIONS_GHC -fllvm #-}
+#endif
 module Twee.Index(
   Index,
   empty,
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -5,7 +5,7 @@
 import Twee.Base
 import Twee.Rule
 import Twee.Equation
-import Twee.Proof(Lemma)
+import Twee.Proof(Proof)
 import qualified Twee.Proof as Proof
 import Twee.CP hiding (Config)
 import Twee.Constraints
@@ -33,7 +33,7 @@
 
 {-# INLINEABLE joinCriticalPair #-}
 joinCriticalPair ::
-  (Function f, Has a (Rule f), Has a (Lemma f)) =>
+  (Function f, Has a (Rule f), Has a (Proof f)) =>
   Config ->
   Index f (Equation f) -> RuleIndex f a ->
   Maybe (Model f) -> -- A model to try before checking ground joinability
@@ -67,7 +67,7 @@
 {-# INLINEABLE step3 #-}
 {-# INLINEABLE allSteps #-}
 step1, step2, step3, allSteps ::
-  (Function f, Has a (Rule f), Has a (Lemma f)) =>
+  (Function f, Has a (Rule f), Has a (Proof f)) =>
   Config -> Index f (Equation f) -> RuleIndex f a -> CriticalPair f -> Maybe (CriticalPair f)
 allSteps config eqns idx cp =
   step1 config eqns idx cp >>=
@@ -104,7 +104,7 @@
 
 {-# INLINEABLE joinWith #-}
 joinWith ::
-  (Has a (Rule f), Has a (Lemma f)) =>
+  (Has a (Rule f), Has a (Proof f)) =>
   Index f (Equation f) -> RuleIndex f a -> (Term f -> Term f -> Resulting f) -> CriticalPair f -> Maybe (CriticalPair f)
 joinWith eqns idx reduce cp@CriticalPair{cp_eqn = lhs :=: rhs, ..}
   | subsumed eqns idx eqn = Nothing
@@ -122,7 +122,7 @@
 
 {-# INLINEABLE subsumed #-}
 subsumed ::
-  (Has a (Rule f), Has a (Lemma f)) =>
+  (Has a (Rule f), Has a (Proof f)) =>
   Index f (Equation f) -> RuleIndex f a -> Equation f -> Bool
 subsumed eqns idx (t :=: u)
   | t == u = True
@@ -146,7 +146,7 @@
 
 {-# INLINEABLE groundJoin #-}
 groundJoin ::
-  (Function f, Has a (Rule f), Has a (Lemma f)) =>
+  (Function f, Has a (Rule f), Has a (Proof f)) =>
   Config -> Index f (Equation f) -> RuleIndex f a -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
 groundJoin config eqns idx ctx cp@CriticalPair{cp_eqn = t :=: u, ..} =
   case partitionEithers (map (solve (usort (atoms t ++ atoms u))) ctx) of
@@ -158,7 +158,7 @@
 
 {-# INLINEABLE groundJoinFrom #-}
 groundJoinFrom ::
-  (Function f, Has a (Rule f), Has a (Lemma f)) =>
+  (Function f, Has a (Rule f), Has a (Proof f)) =>
   Config -> Index f (Equation f) -> RuleIndex f a -> Model f -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
 groundJoinFrom config@Config{..} eqns idx model ctx cp@CriticalPair{cp_eqn = t :=: u, ..}
   | not cfg_ground_join ||
@@ -197,7 +197,7 @@
 
 {-# INLINEABLE groundJoinFromMaybe #-}
 groundJoinFromMaybe ::
-  (Function f, Has a (Rule f), Has a (Lemma f)) =>
+  (Function f, Has a (Rule f), Has a (Proof f)) =>
   Config -> Index f (Equation f) -> RuleIndex f a -> Maybe (Model f) -> [Branch f] -> CriticalPair f -> Either (Model f) [CriticalPair f]
 groundJoinFromMaybe config eqns idx Nothing = groundJoin config eqns idx
 groundJoinFromMaybe config eqns idx (Just model) = groundJoinFrom config eqns idx model
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -2,7 +2,7 @@
 {-# LANGUAGE TypeFamilies, PatternGuards, RecordWildCards, ScopedTypeVariables #-}
 module Twee.Proof(
   -- * Constructing proofs
-  Proof, Derivation(..), Lemma(..), Axiom(..),
+  Proof, Derivation(..), Axiom(..),
   certify, equation, derivation,
   -- ** Smart constructors for derivations
   lemma, axiom, symm, trans, cong, congPath,
@@ -37,13 +37,13 @@
   Proof {
     equation   :: !(Equation f),
     derivation :: !(Derivation f) }
-  deriving (Eq, Show)
+  deriving Show
 
 -- | A derivation is an unchecked proof. It might be wrong!
 -- The way to check it is to call 'certify' to turn it into a 'Proof'.
 data Derivation f =
     -- | Apply an existing rule (with proof!) to the root of a term
-    UseLemma {-# UNPACK #-} !(Lemma f) !(Subst f)
+    UseLemma {-# UNPACK #-} !(Proof f) !(Subst f)
     -- | Apply an axiom to the root of a term
   | UseAxiom {-# UNPACK #-} !(Axiom f) !(Subst f)
     -- | Reflexivity. @'Refl' t@ proves @t = t@.
@@ -58,16 +58,6 @@
   | Cong {-# UNPACK #-} !(Fun f) ![Derivation f]
   deriving (Eq, Show)
 
--- | A lemma, which includes a proof.
-data Lemma f =
-  Lemma {
-    -- | The id number of the lemma.
-    -- Has no semantic meaning; for convenience only.
-    lemma_id :: {-# UNPACK #-} !Id,
-    -- | A proof of the lemma.
-    lemma_proof :: !(Proof f) }
-  deriving Show
-
 --  | An axiom, which comes without proof.
 data Axiom f =
   Axiom {
@@ -95,8 +85,8 @@
     Nothing -> error ("Invalid proof created!\n" ++ prettyShow p)
     Just eqn -> Proof eqn p
   where
-    check (UseLemma Lemma{..} sub) =
-      return (subst sub (equation lemma_proof))
+    check (UseLemma proof sub) =
+      return (subst sub (equation proof))
     check (UseAxiom Axiom{..} sub) =
       return (subst sub axiom_eqn)
     check (Refl t) =
@@ -124,14 +114,12 @@
 ----------------------------------------------------------------------
 
 -- Typeclass instances.
-instance Eq (Lemma f) where
+instance Eq (Proof f) where
   x == y = compare x y == EQ
-instance Ord (Lemma f) where
-  compare =
-    comparing (\x ->
-      -- Don't look into lemma proofs when comparing derivations,
-      -- to avoid exponential blowup
-      (lemma_id x, equation (lemma_proof x)))
+instance Ord (Proof f) where
+  -- Don't look at the proof itself, to prevent exponential blowup
+  -- when a proof contains UseLemma
+  compare = comparing equation
 
 instance Symbolic (Derivation f) where
   type ConstantOf (Derivation f) = f
@@ -150,10 +138,10 @@
   subst_ sub (Cong f ps) = cong f (subst_ sub ps)
 
 instance Function f => Pretty (Proof f) where
-  pPrint = pPrintLemma defaultConfig prettyShow
+  pPrint = pPrintLemma defaultConfig (prettyShow . axiom_number) (prettyShow . equation)
 instance PrettyTerm f => Pretty (Derivation f) where
   pPrint (UseLemma lemma sub) =
-    text "subst" <#> pPrintTuple [pPrint lemma, pPrint sub]
+    text "subst" <#> pPrintTuple [text "lemma" <#> pPrint (equation lemma), pPrint sub]
   pPrint (UseAxiom axiom sub) =
     text "subst" <#> pPrintTuple [pPrint axiom, pPrint sub]
   pPrint (Refl t) =
@@ -170,11 +158,6 @@
     text "axiom" <#>
     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
 
-instance PrettyTerm f => Pretty (Lemma f) where
-  pPrint Lemma{..} =
-    text "lemma" <#>
-    pPrintTuple [pPrint lemma_id, pPrint (equation lemma_proof)]
-
 -- | Simplify a derivation.
 --
 -- After simplification, a derivation has the following properties:
@@ -182,25 +165,25 @@
 --   * 'Symm' is pushed down next to 'Lemma' and 'Axiom'
 --   * 'Refl' only occurs inside 'Cong' or at the top level
 --   * 'Trans' is right-associated and is pushed inside 'Cong' if possible
-simplify :: Minimal f => (Lemma f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
+simplify :: Minimal f => (Proof f -> Maybe (Derivation f)) -> Derivation f -> Derivation f
 simplify lem p = simp p
   where
-    simp p@(UseLemma lemma sub) =
-      case lem lemma of
+    simp p@(UseLemma q sub) =
+      case lem q of
         Nothing -> p
-        Just q ->
+        Just r ->
           let
             -- Get rid of any variables that are not bound by sub
             -- (e.g., ones which only occur internally in q)
-            dead = usort (vars q) \\ substDomain sub
-          in simp (subst sub (erase dead q))
+            dead = usort (vars r) \\ substDomain sub
+          in simp (subst sub (erase dead r))
     simp (Symm p) = symm (simp p)
     simp (Trans p q) = trans (simp p) (simp q)
     simp (Cong f ps) = cong f (map simp ps)
     simp p = p
 
-lemma :: Lemma f -> Subst f -> Derivation f
-lemma lem@Lemma{..} sub = UseLemma lem sub
+lemma :: Proof f -> Subst f -> Derivation f
+lemma p sub = UseLemma p sub
 
 axiom :: Axiom f -> Derivation f
 axiom ax@Axiom{..} =
@@ -244,15 +227,15 @@
     unRefl _ = Nothing
 
 -- | Find all lemmas which are used in a derivation.
-usedLemmas :: Derivation f -> [Lemma f]
+usedLemmas :: Derivation f -> [Proof f]
 usedLemmas p = map fst (usedLemmasAndSubsts p)
 
 -- | Find all lemmas which are used in a derivation,
 -- together with the substitutions used.
-usedLemmasAndSubsts :: Derivation f -> [(Lemma f, Subst f)]
+usedLemmasAndSubsts :: Derivation f -> [(Proof f, Subst f)]
 usedLemmasAndSubsts p = lem p []
   where
-    lem (UseLemma lemma sub) = ((lemma, sub):)
+    lem (UseLemma p sub) = ((p, sub):)
     lem (Symm p) = lem p
     lem (Trans p q) = lem p . lem q
     lem (Cong _ ps) = foldr (.) id (map lem ps)
@@ -313,7 +296,7 @@
     -- | The used axioms.
     pres_axioms :: [Axiom f],
     -- | The used lemmas.
-    pres_lemmas :: [Lemma f],
+    pres_lemmas :: [Proof f],
     -- | The goals proved.
     pres_goals  :: [ProvedGoal f] }
   deriving Show
@@ -367,18 +350,19 @@
 present config goals =
   -- First find all the used lemmas, then hand off to presentWithGoals
   presentWithGoals config goals
-    (used Set.empty (concatMap (usedLemmas . derivation . pg_proof) goals))
+    (snd (used Set.empty (concatMap (usedLemmas . derivation . pg_proof) goals)))
   where
-    used lems [] = Set.elems lems
+    used lems [] = (lems, [])
     used lems (x:xs)
       | x `Set.member` lems = used lems xs
       | otherwise =
-        used (Set.insert x lems)
-          (usedLemmas (derivation (lemma_proof x)) ++ xs)
+        let (lems1, ys) = used (Set.insert x lems) (usedLemmas (derivation x))
+            (lems2, zs) = used lems1 xs
+        in (lems2, ys ++ [x] ++ zs)
 
 presentWithGoals ::
   Function f =>
-  Config -> [ProvedGoal f] -> [Lemma f] -> Presentation f
+  Config -> [ProvedGoal f] -> [Proof f] -> Presentation f
 presentWithGoals config@Config{..} goals lemmas
   -- We inline a lemma if one of the following holds:
   --   * It only has one step
@@ -392,11 +376,10 @@
     let
       axioms = usort $
         concatMap (usedAxioms . derivation . pg_proof) goals ++
-        concatMap (usedAxioms . derivation . lemma_proof) lemmas
+        concatMap (usedAxioms . derivation) lemmas
     in
       Presentation axioms
-        [ lemma { lemma_proof = flattenProof lemma_proof }
-        | lemma@Lemma{..} <- lemmas ]
+        (map flattenProof lemmas)
         [ decodeGoal (goal { pg_proof = flattenProof pg_proof })
         | goal@ProvedGoal{..} <- goals ]
 
@@ -408,8 +391,8 @@
         [ decodeGoal (goal { pg_proof = certify $ simplify inline (derivation pg_proof) })
         | goal@ProvedGoal{..} <- goals ]
       lemmas' =
-        [ Lemma n (certify $ simplify inline (derivation p))
-        | lemma@(Lemma n p) <- lemmas, not (lemma `Map.member` inlinings) ]
+        [ certify $ simplify inline (derivation lemma)
+        | lemma <- lemmas, not (lemma `Map.member` inlinings) ]
     in
       presentWithGoals config goals' lemmas'
 
@@ -419,25 +402,26 @@
         [ (lemma, p)
         | lemma <- lemmas, Just p <- [tryInline lemma]]
 
-    tryInline (Lemma n p)
-      | shouldInline n p = Just (derivation p)
-    tryInline (Lemma n p)
+    tryInline p
+      | shouldInline p = Just (derivation p)
+    tryInline p
       -- Check for subsumption by an earlier lemma
-      | Just (Lemma m q) <- Map.lookup (canonicalise (t :=: u)) equations, m < n =
+      | Just (m, q) <- Map.lookup (canonicalise (t :=: u)) equations, m < n =
         Just (subsume p (derivation q))
-      | Just (Lemma m q) <- Map.lookup (canonicalise (u :=: t)) equations, m < n =
+      | Just (m, q) <- Map.lookup (canonicalise (u :=: t)) equations, m < n =
         Just (subsume p (Symm (derivation q)))
       where
         t :=: u = equation p
+        Just (n, _) = Map.lookup (canonicalise (equation p)) equations
     tryInline _ = Nothing
 
-    shouldInline n p =
+    shouldInline p =
       cfg_no_lemmas ||
       oneStep (derivation p) ||
       (not cfg_all_lemmas &&
        (isJust (decodeEquality (eqn_lhs (equation p))) ||
         isJust (decodeEquality (eqn_rhs (equation p))) ||
-        Map.lookup n uses == Just 1))
+        Map.lookup p uses == Just 1))
   
     subsume p q =
       -- Rename q so its variables match p's
@@ -450,17 +434,17 @@
     -- Record which lemma proves each equation
     equations =
       Map.fromList
-        [ (canonicalise (equation lemma_proof), lemma)
-        | lemma@Lemma{..} <- lemmas]
+        [ (canonicalise (equation p), (i, p))
+        | (i, p) <- zip [0..] lemmas]
 
     -- Count how many times each lemma is used
     uses =
       Map.fromListWith (+)
-        [ (lemma_id, 1)
-        | Lemma{..} <-
+        [ (p, 1)
+        | p <-
             concatMap usedLemmas
               (map (derivation . pg_proof) goals ++
-               map (derivation . lemma_proof) lemmas) ]
+               map derivation lemmas) ]
 
     -- Check if a proof only has one step.
     -- Trans only occurs at the top level by this point.
@@ -471,8 +455,8 @@
 invisible (t :=: u) = show (pPrint t) == show (pPrint u)
 
 -- Pretty-print the proof of a single lemma.
-pPrintLemma :: Function f => Config -> (Id -> String) -> Proof f -> Doc
-pPrintLemma Config{..} lemmaName p =
+pPrintLemma :: Function f => Config -> (Axiom f -> String) -> (Proof f -> String) -> Proof f -> Doc
+pPrintLemma Config{..} axiomNum lemmaNum p =
   ppTerm (eqn_lhs (equation q)) $$ pp (derivation q)
   where
     q = flattenProof p
@@ -496,10 +480,10 @@
       text "and" <+>
       text (last xs)
 
-    ppLemma (Lemma{..}, sub) =
-      text "lemma" <+> text (lemmaName lemma_id) <#> showSubst sub
-    ppAxiom (Axiom{..}, sub) =
-      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <#> showSubst sub
+    ppLemma (p, sub) =
+      text "lemma" <+> text (lemmaNum p) <#> showSubst sub
+    ppAxiom (axiom@Axiom{..}, sub) =
+      text "axiom" <+> text (axiomNum axiom) <+> parens (text axiom_name) <#> showSubst sub
 
     showSubst sub
       | cfg_show_instances && not (null (substToList sub)) =
@@ -575,11 +559,11 @@
 pPrintPresentation :: forall f. Function f => Config -> Presentation f -> Doc
 pPrintPresentation config (Presentation axioms lemmas goals) =
   vcat $ intersperse (text "") $
-    vcat [ describeEquation "Axiom" (show n) (Just name) eqn
-         | Axiom n name eqn <- axioms,
+    vcat [ describeEquation "Axiom" (axiomNum axiom) (Just name) eqn
+         | axiom@(Axiom _ name eqn) <- axioms,
            not (invisible eqn) ]:
-    [ pp "Lemma" (num n) Nothing (equation p) emptySubst p
-    | Lemma n p <- lemmas,
+    [ pp "Lemma" (lemmaNum p) Nothing (equation p) emptySubst p
+    | p <- lemmas,
       not (invisible (equation p)) ] ++
     [ pp "Goal" (show num) (Just pg_name) pg_goal_hint pg_witness_hint pg_proof
     | (num, ProvedGoal{..}) <- zip [1..] goals ]
@@ -588,11 +572,12 @@
       describeEquation kind n mname eqn $$
       ppWitness witness $$
       text "Proof:" $$
-      pPrintLemma config num p
+      pPrintLemma config axiomNum lemmaNum p
 
-    num x = show (fromJust (Map.lookup x nums))
-    nums = Map.fromList (zip (map lemma_id lemmas) [n+1 ..])
-    n = maximum $ 0:map axiom_number axioms
+    axiomNums = Map.fromList (zip axioms [1..])
+    lemmaNums = Map.fromList (zip lemmas [length axioms+1..])
+    axiomNum x = show (fromJust (Map.lookup x axiomNums))
+    lemmaNum x = show (fromJust (Map.lookup x lemmaNums))
 
     ppWitness sub
       | sub == emptySubst = pPrintEmpty
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -18,7 +18,7 @@
 import Data.Ord
 import Twee.Equation
 import qualified Twee.Proof as Proof
-import Twee.Proof(Derivation, Lemma(..))
+import Twee.Proof(Derivation, Proof)
 import Data.Tuple
 
 --------------------------------------------------------------------------------
@@ -229,7 +229,7 @@
 -- | A multi-step rewrite proof @t ->* u@
 data Reduction f =
     -- | Apply a single rewrite rule to the root of a term
-    Step {-# UNPACK #-} !(Lemma f) !(Rule f) !(Subst f)
+    Step {-# UNPACK #-} !(Proof f) !(Rule f) !(Subst f)
     -- | Reflexivity
   | Refl {-# UNPACK #-} !(Term f)
     -- | Transivitity
@@ -290,7 +290,7 @@
 
 -- | Construct a basic rewrite step.
 {-# INLINE step #-}
-step :: (Has a (Rule f), Has a (Lemma f)) => a -> Subst f -> Reduction f
+step :: (Has a (Rule f), Has a (Proof f)) => a -> Subst f -> Reduction f
 step x sub = Step (the x) (the x) sub
 
 ----------------------------------------------------------------------
@@ -420,14 +420,14 @@
 
 -- | A strategy which rewrites using an index.
 {-# INLINE rewrite #-}
-rewrite :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
+rewrite :: (Function f, Has a (Rule f), Has a (Proof f)) => (Rule f -> Subst f -> Bool) -> Index f a -> Strategy f
 rewrite p rules t = do
   rule <- Index.approxMatches t rules
   tryRule p rule t
 
 -- | A strategy which applies one rule only.
 {-# INLINEABLE tryRule #-}
-tryRule :: (Function f, Has a (Rule f), Has a (Lemma f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
+tryRule :: (Function f, Has a (Rule f), Has a (Proof f)) => (Rule f -> Subst f -> Bool) -> a -> Strategy f
 tryRule p rule t = do
   sub <- maybeToList (match (lhs (the rule)) t)
   guard (p (the rule) sub)
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -13,7 +13,11 @@
 --   * substitutions ('Substitution', 'Subst', 'subst');
 --   * unification ('unify') and matching ('match');
 --   * miscellaneous useful functions on terms.
-{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables #-}
+{-# LANGUAGE BangPatterns, PatternSynonyms, ViewPatterns, TypeFamilies, OverloadedStrings, ScopedTypeVariables, CPP #-}
+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
+#ifdef USE_LLVM
+{-# OPTIONS_GHC -fllvm #-}
+#endif
 module Twee.Term(
   -- * Terms
   Term, pattern Var, pattern App, isApp, isVar, singleton, len,
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -3,7 +3,11 @@
 -- and provides primitives for building higher-level stuff.
 {-# LANGUAGE CPP, PatternSynonyms, ViewPatterns,
     MagicHash, UnboxedTuples, BangPatterns,
-    RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving #-}
+    RankNTypes, RecordWildCards, GeneralizedNewtypeDeriving, CPP #-}
+{-# OPTIONS_GHC -O2 -fmax-worker-args=100 #-}
+#ifdef USE_LLVM
+{-# OPTIONS_GHC -fllvm #-}
+#endif
 module Twee.Term.Core where
 
 import Data.Primitive(sizeOf)
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.1.5
+version:             2.2
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -29,14 +29,6 @@
   location: git://github.com/nick8325/twee.git
   branch:   master
 
-flag static
-  description: Build a static binary.
-  default: False
-
-flag static-cxx
-  description: Build a binary which statically links against libstdc++.
-  default: False
-
 flag llvm
   description: Build using LLVM backend for faster code.
   default: False
@@ -80,11 +72,11 @@
     primitive >= 0.6.2.0,
     vector
   hs-source-dirs:      .
-  ghc-options:         -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100
+  ghc-options:         -W -fno-warn-incomplete-patterns
   default-language:    Haskell2010
 
   if flag(llvm)
-    ghc-options: -fllvm
+    cpp-options: -DUSE_LLVM
   if flag(bounds-checks)
     cpp-options: -DBOUNDS_CHECKS
     exposed-modules: