diff --git a/executable/Main.hs b/executable/Main.hs
--- a/executable/Main.hs
+++ b/executable/Main.hs
@@ -217,7 +217,7 @@
       Main.isEquals fun
 
 isType :: Jukebox.Function -> Bool
-isType fun = "$to_" `isPrefixOf` base (name fun)
+isType fun = "$to_" `isPrefixOf` base (name fun) && Jukebox.arity fun == 1
 
 isIfeq :: Jukebox.Function -> Bool
 isIfeq fun = "$ifeq" `isPrefixOf` base (name fun)
@@ -437,7 +437,7 @@
       pPrintTerm uncurried prettyNormal 0 (text f) xs
 
     step :: String -> [Doc] -> Doc
-    step f xs = traceApp "step" [traceApp f xs] <> text "."
+    step f xs = traceApp "step" [traceApp f xs] <#> text "."
 
   say "Here is the input problem:"
   forM_ axioms $ \Axiom{..} ->
@@ -460,7 +460,7 @@
     sayTrace ""
     forM_ (pres_lemmas pres) $ \Lemma{..} ->
       sayTrace $ show $
-        traceApp "lemma" [traceEqn (equation lemma_proof)] <> text "."
+        traceApp "lemma" [traceEqn (equation lemma_proof)] <#> text "."
 
     when tstp $ do
       putStrLn "% SZS output start CNFRefutation"
diff --git a/misc/bench.hs b/misc/bench.hs
--- a/misc/bench.hs
+++ b/misc/bench.hs
@@ -1,24 +1,24 @@
 {-# LANGUAGE PatternGuards, FlexibleInstances #-}
 import Criterion.Main
-import Twee.Term hiding (isFun)
+import Twee.Term hiding (isFun, F)
 import qualified Twee.Term
-import Test.QuickCheck
+import Test.QuickCheck hiding (Fun)
 import Data.Int
 import Data.Maybe
 import Twee.Term.Core hiding (subst)
 
-instance Num (Fun Int) where fromInteger n = F (fromInteger n) (fromInteger n)
+instance Num (Fun Int) where fromInteger n = F (fromInteger n)
 instance Num Var where fromInteger = V . fromInteger
 
 t0, t1, u0, u1, t2, t, u :: Term Int
-t0 = build $ fun 0 [var 0, fun 0 [var 0, fun 0 [fun 0 [var 0, var 1], var 2]]]
-u0 = build $ fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 0 [fun 0 [fun 0 [fun 2 [fun 2 [var 2, var 2], var 1], fun 0 [fun 2 [var 2, var 2], var 3]], fun 2 [fun 2 [var 2, var 2], var 1]], fun 2 [var 2, var 2]]]]
+t0 = build $ app 0 [var 0, app 0 [var 0, app 0 [app 0 [var 0, var 1], var 2]]]
+u0 = build $ app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 0 [app 0 [app 0 [app 2 [app 2 [var 2, var 2], var 1], app 0 [app 2 [var 2, var 2], var 3]], app 2 [app 2 [var 2, var 2], var 1]], app 2 [var 2, var 2]]]]
 
-t1 = build $ fun 0 [fun 1 [var 0], fun 1 [var 1]]
-u1 = build $ fun 0 [fun 1 [fun 0 [fun 2 emptyTermList, fun 3 emptyTermList]], fun 1 [fun 0 [fun 4 emptyTermList, fun 5 emptyTermList]]]
+t1 = build $ app 0 [app 1 [var 0], app 1 [var 1]]
+u1 = build $ app 0 [app 1 [app 0 [app 2 empty, app 3 empty]], app 1 [app 0 [app 4 empty, app 5 empty]]]
 
-t2 = build $ fun 0 [var 0, fun 1 [var 1, fun 1 [var 1, var 1]]]
-u2 = build $ fun 0 [fun 0 [var 2, var 2], var 2]
+t2 = build $ app 0 [var 0, app 1 [var 1, app 1 [var 1, var 1]]]
+u2 = build $ app 0 [app 0 [var 2, var 2], var 2]
 
 t = t0
 u = u0
@@ -61,7 +61,7 @@
     bench "unify-subst-closed2" (whnf (build . uncurry subst) (csub', u2)),
     bench "mgu-tri" (whnf (uncurry mgu1) (t2, u2)),
     bench "mgu-close" (whnf (uncurry mgu2) (t2, u2)),
-    bench "make-constant" (whnf (build . uncurry fun) (F 0 0, emptyTermList)),
+    bench "make-constant" (whnf (build . uncurry app) (F 0, empty)),
     bench "baseline" (whnf (uncurry (+)) (0 :: Int, 0))]
 
 prop :: Bool -> NonNegative (Small Int) -> NonNegative (Small Int) -> Property
diff --git a/twee.cabal b/twee.cabal
--- a/twee.cabal
+++ b/twee.cabal
@@ -1,5 +1,5 @@
 name:                twee
-version:             2.1.4
+version:             2.1.5
 synopsis:            An equational theorem prover
 homepage:            http://github.com/nick8325/twee
 license:             BSD3
@@ -44,11 +44,11 @@
   main-is:             executable/Main.hs
   default-language:    Haskell2010
   build-depends:       base < 5,
-                       twee-lib == 2.1.4,
+                       twee-lib == 2.1.5,
                        containers,
                        pretty,
                        split,
-                       jukebox >= 0.3.2
+                       jukebox >= 0.3.5
   ghc-options:         -W -fno-warn-incomplete-patterns -O2 -fmax-worker-args=100
 
   if flag(llvm)