diff --git a/Twee.hs b/Twee.hs
--- a/Twee.hs
+++ b/Twee.hs
@@ -122,7 +122,7 @@
   pPrint (NewEquation eqn) =
     text "  (hard)" <+> pPrint eqn
   pPrint (DeleteActive rule) =
-    text "  (delete rule " <> pPrint (active_id rule) <> text ")"
+    text "  (delete rule " <#> pPrint (active_id rule) <#> text ")"
   pPrint SimplifyQueue =
     text "  (simplifying queued critical pairs...)"
   pPrint Interreduce =
@@ -293,7 +293,7 @@
 
 instance Function f => Pretty (Active f) where
   pPrint Active{..} =
-    pPrint active_id <> text "." <+> pPrint (canonicalise active_rule)
+    pPrint active_id <#> text "." <+> pPrint (canonicalise active_rule)
 
 instance Has (ActiveRule f) Id where the = rule_active
 instance Has (ActiveRule f) RuleId where the = rule_rid
diff --git a/Twee/Base.hs b/Twee/Base.hs
--- a/Twee/Base.hs
+++ b/Twee/Base.hs
@@ -254,7 +254,7 @@
 
 instance Pretty f => Pretty (Extended f) where
   pPrintPrec _ _ Minimal = text "?"
-  pPrintPrec _ _ (Skolem (V n)) = text "sk" <> pPrint n
+  pPrintPrec _ _ (Skolem (V n)) = text "sk" <#> pPrint n
   pPrintPrec l p (Function f) = pPrintPrec l p f
 
 instance PrettyTerm f => PrettyTerm (Extended f) where
diff --git a/Twee/Join.hs b/Twee/Join.hs
--- a/Twee/Join.hs
+++ b/Twee/Join.hs
@@ -81,7 +81,10 @@
     case cp_top cp of
       Just top ->
         case (join (cp, top), join (flipCP (cp, top))) of
-          (Just _, Just _) -> Just cp
+          (Just cp1, Just cp2) ->
+            case simplerThan (cp_eqn cp1) (cp_eqn cp2) of
+              True -> Just cp1
+              False -> Just cp2
           _ -> Nothing
       _ -> Just cp
   where
diff --git a/Twee/Pretty.hs b/Twee/Pretty.hs
--- a/Twee/Pretty.hs
+++ b/Twee/Pretty.hs
@@ -3,7 +3,7 @@
 {-# LANGUAGE Rank2Types #-}
 module Twee.Pretty(module Twee.Pretty, module Text.PrettyPrint.HughesPJClass, Pretty(..)) where
 
-import Text.PrettyPrint.HughesPJClass hiding (empty)
+import Text.PrettyPrint.HughesPJClass hiding (empty, (<>))
 import qualified Text.PrettyPrint.HughesPJClass as PP
 import qualified Data.Map as Map
 import Data.Map(Map)
@@ -18,6 +18,12 @@
 prettyPrint :: Pretty a => a -> IO ()
 prettyPrint x = putStrLn (prettyShow x)
 
+-- | Put one document beside another, i.e., 'PP.<>'.
+-- Renamed here because (a different) '<>' is exported by "Prelude".
+infixl 6 <#>
+(<#>) :: Doc -> Doc -> Doc
+(<#>) = (PP.<>)
+
 -- | The empty document. Used to avoid name clashes with 'Twee.Term.empty'.
 pPrintEmpty :: Doc
 pPrintEmpty = PP.empty
@@ -53,7 +59,7 @@
 instance (Eq a, Integral a, Pretty a) => Pretty (Ratio a) where
   pPrint a
     | denominator a == 1 = pPrint (numerator a)
-    | otherwise = text "(" <+> pPrint (numerator a) <> text "/" <> pPrint (denominator a) <+> text ")"
+    | otherwise = text "(" <+> pPrint (numerator a) <#> text "/" <#> pPrint (denominator a) <+> text ")"
 
 -- | Generate a list of candidate names for pretty-printing.
 supply :: [String] -> [String]
@@ -78,7 +84,7 @@
   pPrintPrec _ _ = pPrint . unpack
 
 instance PrettyTerm f => Pretty (Subst f) where
-  pPrint sub = text "{" <> fsep (punctuate (text ",") docs) <> text "}"
+  pPrint sub = text "{" <#> fsep (punctuate (text ",") docs) <#> text "}"
     where
       docs =
         [ hang (pPrint x <+> text "->") 2 (pPrint t)
@@ -130,7 +136,7 @@
     let
       f [] = d
       f xs =
-        d <> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))
+        d <#> parens (hsep (punctuate comma (map (pPrintPrec l 0) xs)))
     in f
 
 -- | A helper function that deals with under- and oversaturated applications.
@@ -158,13 +164,13 @@
 prefix =
   fixedArity 1 $
   TermStyle $ \l _ d [x] ->
-    d <> pPrintPrec l 11 x
+    d <#> pPrintPrec l 11 x
 
 -- | For postfix operators.
 postfix =
   fixedArity 1 $
   TermStyle $ \l _ d [x] ->
-    pPrintPrec l 11 x <> d
+    pPrintPrec l 11 x <#> d
 
 -- | For infix operators.
 infixStyle :: Int -> TermStyle
diff --git a/Twee/Proof.hs b/Twee/Proof.hs
--- a/Twee/Proof.hs
+++ b/Twee/Proof.hs
@@ -117,7 +117,10 @@
 
 ----------------------------------------------------------------------
 -- Everything below this point need not be trusted, since all proof
--- construction goes through the "proof" function.
+-- construction goes through the "certify" function.
+--
+-- N.B.: For this reason, the code below must never directly invoke
+-- the Proof constructor!
 ----------------------------------------------------------------------
 
 -- Typeclass instances.
@@ -150,26 +153,26 @@
   pPrint = pPrintLemma defaultConfig prettyShow
 instance PrettyTerm f => Pretty (Derivation f) where
   pPrint (UseLemma lemma sub) =
-    text "subst" <> pPrintTuple [pPrint lemma, pPrint sub]
+    text "subst" <#> pPrintTuple [pPrint lemma, pPrint sub]
   pPrint (UseAxiom axiom sub) =
-    text "subst" <> pPrintTuple [pPrint axiom, pPrint sub]
+    text "subst" <#> pPrintTuple [pPrint axiom, pPrint sub]
   pPrint (Refl t) =
-    text "refl" <> pPrintTuple [pPrint t]
+    text "refl" <#> pPrintTuple [pPrint t]
   pPrint (Symm p) =
-    text "symm" <> pPrintTuple [pPrint p]
+    text "symm" <#> pPrintTuple [pPrint p]
   pPrint (Trans p q) =
-    text "trans" <> pPrintTuple [pPrint p, pPrint q]
+    text "trans" <#> pPrintTuple [pPrint p, pPrint q]
   pPrint (Cong f ps) =
-    text "cong" <> pPrintTuple (pPrint f:map pPrint ps)
+    text "cong" <#> pPrintTuple (pPrint f:map pPrint ps)
 
 instance PrettyTerm f => Pretty (Axiom f) where
   pPrint Axiom{..} =
-    text "axiom" <>
+    text "axiom" <#>
     pPrintTuple [pPrint axiom_number, text axiom_name, pPrint axiom_eqn]
 
 instance PrettyTerm f => Pretty (Lemma f) where
   pPrint Lemma{..} =
-    text "lemma" <>
+    text "lemma" <#>
     pPrintTuple [pPrint lemma_id, pPrint (equation lemma_proof)]
 
 -- | Simplify a derivation.
@@ -353,7 +356,7 @@
     error $ show $
       text "Invalid ProvedGoal!" $$
       text "Claims to prove" <+> pPrint pg_goal_hint $$
-      text "with witness" <+> pPrint pg_witness_hint <> text "," $$
+      text "with witness" <+> pPrint pg_witness_hint <#> text "," $$
       text "but actually proves" <+> pPrint (equation pg_proof)
 
 instance Function f => Pretty (Presentation f) where
@@ -484,7 +487,7 @@
        text "}" $$
        ppTerm (eqn_rhs (equation (certify p))))
 
-    ppTerm t = text "  " <> pPrint t
+    ppTerm t = text "  " <#> pPrint t
 
     ppStep [] = text "reflexivity" -- ??
     ppStep [x] = text x
@@ -494,13 +497,13 @@
       text (last xs)
 
     ppLemma (Lemma{..}, sub) =
-      text "lemma" <+> text (lemmaName lemma_id) <> showSubst sub
+      text "lemma" <+> text (lemmaName lemma_id) <#> showSubst sub
     ppAxiom (Axiom{..}, sub) =
-      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <> showSubst sub
+      text "axiom" <+> pPrint axiom_number <+> parens (text axiom_name) <#> showSubst sub
 
     showSubst sub
       | cfg_show_instances && not (null (substToList sub)) =
-        text " with " <>
+        text " with " <#>
         fsep (punctuate comma
           [ pPrint x <+> text "->" <+> pPrint t
           | (x, t) <- substToList sub ])
@@ -612,11 +615,11 @@
   PrettyTerm f =>
   String -> String -> Maybe String -> Equation f -> Doc
 describeEquation kind num mname eqn =
-  text kind <+> text num <>
+  text kind <+> text num <#>
   (case mname of
      Nothing -> text ""
-     Just name -> text (" (" ++ name ++ ")")) <>
-  text ":" <+> pPrint eqn <> text "."
+     Just name -> text (" (" ++ name ++ ")")) <#>
+  text ":" <+> pPrint eqn <#> text "."
 
 ----------------------------------------------------------------------
 -- Making proofs of existential goals more readable.
diff --git a/Twee/Rule.hs b/Twee/Rule.hs
--- a/Twee/Rule.hs
+++ b/Twee/Rule.hs
@@ -489,4 +489,6 @@
   reducesWith (\t u -> lessEq (subst skolemise t) (subst skolemise u)) rule sub
   where
     skolemise (V x) = con (skolem (V (x + k)))
+    -- Make sure the Skolem constants we choose don't overlap with any
+    -- already in the rule
     V k = maximum (V 0:map succ (catMaybes (map getSkolem (funs rule))))
diff --git a/Twee/Term.hs b/Twee/Term.hs
--- a/Twee/Term.hs
+++ b/Twee/Term.hs
@@ -62,7 +62,7 @@
 import Twee.Term.Core hiding (F)
 import Data.List hiding (lookup, find)
 import Data.Maybe
-import Data.Monoid
+import Data.Semigroup(Semigroup(..))
 import Data.IntMap.Strict(IntMap)
 import qualified Data.IntMap.Strict as IntMap
 
diff --git a/Twee/Term/Core.hs b/Twee/Term/Core.hs
--- a/Twee/Term/Core.hs
+++ b/Twee/Term/Core.hs
@@ -21,6 +21,7 @@
 import Data.Ord
 import Twee.Label
 import Data.Typeable
+import Data.Semigroup(Semigroup(..))
 
 --------------------------------------------------------------------------------
 -- Symbols. A symbol is a single function or variable in a flatterm.
@@ -281,11 +282,14 @@
 
 type Builder1 s f = State# s -> MutableByteArray# s -> Int# -> Int# -> (# State# s, Int# #)
 
+instance Semigroup (Builder f) where
+  {-# INLINE (<>) #-}
+  Builder m1 <> Builder m2 = Builder (m1 `then_` m2)
 instance Monoid (Builder f) where
   {-# INLINE mempty #-}
   mempty = Builder built
   {-# INLINE mappend #-}
-  Builder m1 `mappend` Builder m2 = Builder (m1 `then_` m2)
+  mappend = (<>)
 
 -- Build a termlist from a Builder.
 -- Works by guessing an appropriate size, and retrying if that was too small.
diff --git a/Twee/Utils.hs b/Twee/Utils.hs
--- a/Twee/Utils.hs
+++ b/Twee/Utils.hs
@@ -58,28 +58,6 @@
     (hSetBuffering stdout buf)
     x
 
-newtype Max a = Max { getMax :: Maybe a }
-
-getMaxWith :: Ord a => a -> Max a -> a
-getMaxWith x (Max (Just y)) = x `max` y
-getMaxWith x (Max Nothing)  = x
-
-instance Ord a => Monoid (Max a) where
-  mempty = Max Nothing
-  Max (Just x) `mappend` y = Max (Just (getMaxWith x y))
-  Max Nothing  `mappend` y = y
-
-newtype Min a = Min { getMin :: Maybe a }
-
-getMinWith :: Ord a => a -> Min a -> a
-getMinWith x (Min (Just y)) = x `min` y
-getMinWith x (Min Nothing)  = x
-
-instance Ord a => Monoid (Min a) where
-  mempty = Min Nothing
-  Min (Just x) `mappend` y = Min (Just (getMinWith x y))
-  Min Nothing  `mappend` y = y
-
 labelM :: Monad m => (a -> m b) -> [a] -> m [(a, b)]
 labelM f = mapM (\x -> do { y <- f x; return (x, y) })
 
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.4
+version:             2.1.5
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3