diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.4
+Version: 0.5.5
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/TPTP/Lexer.x b/src/Jukebox/TPTP/Lexer.x
--- a/src/Jukebox/TPTP/Lexer.x
+++ b/src/Jukebox/TPTP/Lexer.x
@@ -19,7 +19,7 @@
 import Data.Char
 import Data.Ratio
 import Codec.Binary.UTF8.String
-import Data.Symbol
+import qualified Data.Symbol as S
 }
 
 $alpha = [a-zA-Z0-9_]
@@ -98,10 +98,10 @@
 
 {
 data Pos = Pos {-# UNPACK #-} !Word {-# UNPACK #-} !Word deriving Show
-data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !Symbol }
+data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !S.Symbol }
            | Defined { defined :: !Defined  }
-           | Var { tokenName :: {-# UNPACK #-} !Symbol }
-           | DistinctObject { tokenName :: {-# UNPACK #-} !Symbol }
+           | Var { tokenName :: {-# UNPACK #-} !S.Symbol }
+           | DistinctObject { tokenName :: {-# UNPACK #-} !S.Symbol }
            | Number { value :: !Integer }
            | Rational { ratValue :: !Rational }
            | Real { ratValue :: !Rational }
@@ -147,10 +147,10 @@
            | Or | And | Not | Iff | Implies | Follows | Xor | Nor | Nand
            | Eq | Neq | ForAll | Exists | Let | LetTerm -- FOF
            | Colon | Times | Plus | FunArrow -- TFF
-           | Other {-# UNPACK #-} !Symbol -- user-defined
+           | Other {-# UNPACK #-} !S.Symbol -- user-defined
              deriving (Eq, Ord)
 
-showPunct :: Punct -> Symbol
+showPunct :: Punct -> S.Symbol
 showPunct x =
   case x of {
     LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";
@@ -161,14 +161,14 @@
     FunArrow -> ">"; LetTerm -> ":-"; Other x -> x }
 
 instance Show Punct where
-  show = unintern . showPunct
+  show = S.unintern . showPunct
 
 p x = const (Punct x)
 k x = Atom x . copy
 d x = const (Defined x)
 
-copy :: String -> Symbol
-copy = intern
+copy :: String -> S.Symbol
+copy = S.intern
 
 unquote :: String -> String
 unquote (_:x)
diff --git a/src/Jukebox/Tools/HornToUnit.hs b/src/Jukebox/Tools/HornToUnit.hs
--- a/src/Jukebox/Tools/HornToUnit.hs
+++ b/src/Jukebox/Tools/HornToUnit.hs
@@ -33,7 +33,6 @@
 import qualified Data.Set as Set
 import qualified Data.Map.Strict as Map
 import Control.Monad.Trans.RWS
-import Control.Monad.Trans.List
 import Control.Monad.Trans.Class
 
 data HornFlags =
@@ -176,7 +175,7 @@
   (prob, funs) <- evalRWST (mapM elim1 prob) () 0
   return (map toInput (usort funs) ++ concat prob)
   where
-    fresh base = lift $ do
+    fresh base = do
       n <- get
       put $! n+1
       return (variant base [name (show n)])
@@ -193,16 +192,16 @@
     elim1 c =
       case partition pos (toLiterals (what c)) of
         ([], _) -> return [c]
-        ([Pos l], ls) -> runListT $ do
+        ([Pos l], ls) -> do
           l <- foldM (encode (tag c)) l ls
-          return c { what = clause [Pos l] }
+          return [c { what = clause [Pos l] }]
         _ ->
           if dropNonHorn flags then
             return []
           else
             lift $ Left c
 
-    encode :: String -> Atomic -> Literal -> ListT (RWST () [(String, Atomic)] Int (Either (Input Clause))) Atomic
+    encode :: String -> Atomic -> Literal -> RWST () [(String, Atomic)] Int (Either (Input Clause)) Atomic
     encode tag (c :=: d) (Neg (a :=: b)) =
       let
         ty1 = typ a
@@ -226,7 +225,7 @@
         -- ifeq(a, b, c, d) = d
         Asymmetric1 -> do
           ifeq <- passiveFresh (variant ifeqName [name ty1, name ty2] ::: FunType [ty1, ty1, ty2, ty2] ty2)
-          (c :=: d) <- return (swap size (c :=: d))
+          ~(c :=: d) <- return (swap size (c :=: d))
           if passivise flags then do
             axiom ("ifeq_axiom", ifeq :@: [x, x, passive c, y] :=: c)
             return (ifeq :@: [a, b, passive c, passive d] :=: d)
@@ -238,8 +237,8 @@
         -- where sigma = FV(a, b, c, d)
         Asymmetric2 -> do
           ifeqName <- fresh freshName
-          (a :=: b) <- return (swap size (a :=: b))
-          (c :=: d) <- return (swap size (c :=: d))
+          ~(a :=: b) <- return (swap size (a :=: b))
+          ~(c :=: d) <- return (swap size (c :=: d))
           let
             vs =
               if passivise flags then
@@ -259,7 +258,7 @@
         -- where sigma = FV(c, d)
         Asymmetric3 -> do
           ifeqName <- fresh freshName
-          (c :=: d) <- return (swap size (c :=: d))
+          ~(c :=: d) <- return (swap size (c :=: d))
           let
             vs =
               if passivise flags then
@@ -276,7 +275,7 @@
       (\(t :=: u) -> if smaller flags then u :=: t else t :=: u) $
       if f t >= f u then (t :=: u) else (u :=: t)
 
-    axiom l = lift $ tell [l]
+    axiom l = tell [l]
 
     toInput (tag, l) =
       Input {