diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.4.5
+Version: 0.5
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/ExternalProvers/E.hs b/src/Jukebox/ExternalProvers/E.hs
--- a/src/Jukebox/ExternalProvers/E.hs
+++ b/src/Jukebox/ExternalProvers/E.hs
@@ -14,6 +14,7 @@
 import Data.Maybe
 import qualified Data.Map.Strict as Map
 import Data.Map(Map)
+import Data.Symbol
 
 data EFlags = EFlags {
   eprover :: String,
@@ -62,8 +63,8 @@
 
 extractAnswer :: Symbolic a => a -> String -> Either Answer [Term]
 extractAnswer prob str = fromMaybe (Left status) (fmap Right answer)
-  where varMap = Map.fromList [(show (name x), x) | x <- vars prob]
-        funMap = Map.fromList [(show (name x), x) | x <- functions prob]
+  where varMap = Map.fromList [(intern (show (name x)), x) | x <- vars prob]
+        funMap = Map.fromList [(intern (show (name x)), x) | x <- functions prob]
         result = lines str
         status = head $
           [Sat Satisfiable Nothing | "# SZS status Satisfiable" <- result] ++
@@ -97,5 +98,5 @@
         terms =
           bracks (term `sepBy1` punct Comma)
           <|> return []
-        lookup :: Ord a => Map String a -> String -> a
+        lookup :: Map Symbol a -> Symbol -> a
         lookup m x = Map.findWithDefault (error "runE: result from E mentions free names") x m
diff --git a/src/Jukebox/Name.hs b/src/Jukebox/Name.hs
--- a/src/Jukebox/Name.hs
+++ b/src/Jukebox/Name.hs
@@ -14,7 +14,7 @@
 
 data Name =
     Fixed !FixedName (Maybe String)
-  | Unique {-# UNPACK #-} !Int64 String (Maybe String) Renamer
+  | Unique {-# UNPACK #-} !Int64 {-# UNPACK #-} !Symbol (Maybe String) Renamer
   | Variant !Name ![Name] Renamer
 
 data FixedName =
@@ -32,7 +32,7 @@
 base x =
   case name x of
     Fixed x _ -> show x
-    Unique _ xs _ _ -> xs
+    Unique _ xs _ _ -> unintern xs
     Variant x _ _ -> base x
 
 label :: Named a => a -> Maybe String
@@ -101,7 +101,7 @@
       Nothing -> ""
       Just l -> "[" ++ l ++ "]"
     where
-      Renaming _ ys = f xs 0
+      Renaming _ ys = f (unintern xs) 0
   show (Variant x xs _) =
     "variant(" ++ show x ++
       concat [", " ++ show x | x <- xs] ++ ")"
@@ -110,8 +110,11 @@
   name :: a -> Name
 
 instance Named [Char] where
-  name x = Fixed (Basic (intern x)) Nothing
+  name x = name (intern x)
 
+instance Named Symbol where
+  name x = Fixed (Basic x) Nothing
+
 instance Named Integer where
   name n = name ("n" ++ show n)
 
@@ -168,4 +171,4 @@
   let idx' = idx+1
   when (idx' < 0) $ error "Name.newName: too many names"
   put $! idx'
-  return $! Unique idx' (base x) (label x) (renamer x)
+  return $! Unique idx' (intern (base x)) (label x) (renamer x)
diff --git a/src/Jukebox/Options.hs b/src/Jukebox/Options.hs
--- a/src/Jukebox/Options.hs
+++ b/src/Jukebox/Options.hs
@@ -18,6 +18,7 @@
 import Data.Monoid
 #endif
 import Data.Semigroup(Semigroup(..))
+import Control.Monad
 
 ----------------------------------------------------------------------
 -- A parser of some kind annotated with a help text of some kind
@@ -158,7 +159,7 @@
 -- it doesn't matter what order we write the options in,
 -- and because f and x might understand the same flags.
 data ParParser a = ParParser
-  { val :: IO a, -- impure so we can put system information in our options records
+  { val :: Either Error (IO a), -- impure so we can put system information in our options records
     peek :: [String] -> ParseResult a }
 
 data ParseResult a
@@ -177,9 +178,9 @@
   fmap f x = pure f <*> x
 
 instance Applicative ParParser where
-  pure x = ParParser (return x) (const (pure x))
+  pure x = ParParser (Right (return x)) (const (pure x))
   ParParser v p <*> ParParser v' p' =
-    ParParser (v <*> v') (\xs -> p xs <*> p' xs)
+    ParParser (liftM2 (<*>) v v') (\xs -> p xs <*> p' xs)
 
 instance Functor ParseResult where
   fmap f x = pure f <*> x
@@ -196,15 +197,15 @@
   No f <*> No x = No (f <*> x)
 
 runPar :: ParParser a -> [String] -> Either Error (IO a)
-runPar p [] = Right (val p)
+runPar p [] = val p
 runPar p xs@(x:_) =
   case peek p xs of
     Yes n p' -> runPar p' (drop n xs)
     No _ -> Left (Mistake ("Didn't recognise option " ++ x))
     Error err -> Left err
 
-await :: (String -> Bool) -> a -> (String -> [String] -> ParseResult a) -> ParParser a
-await p def par = ParParser (return def) f
+await :: (String -> Bool) -> Either Error a -> (String -> [String] -> ParseResult a) -> ParParser a
+await p def par = ParParser (return <$> def) f
   where f (x:xs) | p x =
           case par x xs of
             Yes n r -> Yes (n+1) r
@@ -228,14 +229,14 @@
   -- The argument parser is given the option name.
   a -> ArgParser (String -> a) -> OptionParser a
 primFlag name help p combine def (Annotated desc (SeqParser args f)) =
-  Annotated [desc'] (await p def (g Right))
+  Annotated [desc'] (await p (Right def) (g Right))
   where desc' = Flag name "General options" NormalMode help (unwords desc)
         g comb x xs =
           case f xs >>= comb . ($ x) of
             Left (Mistake err) -> Error (Mistake ("Error in option --" ++ name ++ ": " ++ err))
             Left (Usage code err) -> Error (Usage code err)
             Right y ->
-              Yes args (await p y (g (combine y)))
+              Yes args (await p (Right y) (g (combine y)))
 
 ----------------------------------------------------------------------
 -- Combinators for building OptionParsers.
@@ -267,15 +268,19 @@
 
 -- A parser that reads all file names from the command line.
 filenames :: OptionParser [String]
-filenames = Annotated [] (from [])
-  where from xs = await p xs (f xs)
-        p x = not ("-" `isPrefixOf` x) || x == "-"
-        f xs y _ = Yes 0 (from (xs ++ [y]))
+filenames = Annotated [] (await p (Left err) (f []))
+  where p x = not ("-" `isPrefixOf` x) || x == "-"
+        f xs y _ = Yes 0 (let ys = xs ++ [y] in await p (Right ys) (f ys))
 
+        err =
+          Usage (ExitFailure 1)
+            ["No input files specified! Try --help.",
+             "You can use \"-\" to read from standard input."]
+
 -- Take a value from the environment.
 io :: IO a -> OptionParser a
 io m = Annotated [] p
-  where p = ParParser m (const (No p))
+  where p = ParParser (Right m) (const (No p))
 
 -- Change the group associated with a set of flags.
 inGroup :: String -> OptionParser a -> OptionParser a
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
@@ -3,12 +3,13 @@
 -- Roughly taken from the TPTP syntax reference
 {
 {-# OPTIONS_GHC -O2 -fno-warn-deprecated-flags #-}
-{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE BangPatterns, OverloadedStrings #-}
 module Jukebox.TPTP.Lexer(
   scan,
   Pos(..),
   Token(..),
   Punct(..),
+  showPunct,
   Defined(..),
   Keyword(..),
   TokenStream(..),
@@ -18,6 +19,7 @@
 import Data.Char
 import Data.Ratio
 import Codec.Binary.UTF8.String
+import Data.Symbol
 }
 
 $alpha = [a-zA-Z0-9_]
@@ -26,6 +28,7 @@
 @dquoted = ($printable # [\\\"]) | \\ $printable
 @pnum = [1-9][0-9]*
 @num  = 0 | @pnum
+@operator = [^\%\(\)\[\]\,\&\|\~\?\!\$'"a-zA-Z0-9_$white]
 
 tokens :-
 -- Comments and whitespace
@@ -71,11 +74,11 @@
 -- Atoms with funny quoted names (here we diverge from the official
 -- syntax, which only allows the escape sequences \\ and \' in quoted
 -- atoms: we allow \ to be followed by any printable character)
-"'"  @quoted+ "'" { Atom Normal . unquote }
+"'"  @quoted+ "'" { Atom Normal . copy . unquote }
 -- Vars are easy :)
 [A-Z][$alpha]* { Var . copy }
 -- Distinct objects, which are double-quoted
-\" @dquoted+  \" { DistinctObject . unquote }
+\" @dquoted+  \" { DistinctObject . copy . unquote }
 -- Numbers
 [\+\-]? @num/($anything # $alpha) { Number . read }
 [\+\-]? @num\/@pnum { Rational . readRational }
@@ -91,17 +94,14 @@
 ":-" { p LetTerm }
 -- Operators (TFF)
 ":" { p Colon }    "*"   { p Times }   "+"  { p Plus }     ">"  { p FunArrow }
--- Operators (THF)
-"^"  { p Lambda } "@" { p Apply }  "!!" { p ForAllLam }  "??"  { p ExistsLam }
-"@+" { p Some }   "@-" { p The }   "<<" { p Subtype }    "-->" { p SequentArrow }
-"!>" { p DependentProduct }        "?*" { p DependentSum }
+@operator+ { \s -> p (Other (copy s)) s }
 
 {
 data Pos = Pos {-# UNPACK #-} !Word {-# UNPACK #-} !Word deriving Show
-data Token = Atom { keyword :: !Keyword, tokenName :: !String }
+data Token = Atom { keyword :: !Keyword, tokenName :: {-# UNPACK #-} !Symbol }
            | Defined { defined :: !Defined  }
-           | Var { tokenName :: !String }
-           | DistinctObject { tokenName :: !String }
+           | Var { tokenName :: {-# UNPACK #-} !Symbol }
+           | DistinctObject { tokenName :: {-# UNPACK #-} !Symbol }
            | Number { value :: !Integer }
            | Rational { ratValue :: !Rational }
            | Real { ratValue :: !Rational }
@@ -147,30 +147,28 @@
            | Or | And | Not | Iff | Implies | Follows | Xor | Nor | Nand
            | Eq | Neq | ForAll | Exists | Let | LetTerm -- FOF
            | Colon | Times | Plus | FunArrow -- TFF
-           | Lambda | Apply | ForAllLam | ExistsLam
-           | DependentProduct | DependentSum | Some | The
-           | Subtype | SequentArrow -- THF
+           | Other {-# UNPACK #-} !Symbol -- user-defined
              deriving (Eq, Ord)
 
+showPunct :: Punct -> Symbol
+showPunct x =
+  case x of {
+    LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";
+    Comma -> ","; Dot -> "."; Or -> "|"; And -> "&"; Not -> "~";
+    Iff -> "<=>"; Implies -> "=>"; Follows -> "<="; Xor -> "<~>";
+    Nor -> "~|"; Nand -> "~&"; Eq -> "="; Neq -> "!="; ForAll -> "!";
+    Exists -> "?"; Let -> ":="; Colon -> ":"; Times -> "*"; Plus -> "+";
+    FunArrow -> ">"; LetTerm -> ":-"; Other x -> x }
+
 instance Show Punct where
-  show x =
-    case x of {
-      LParen -> "("; RParen -> ")"; LBrack -> "["; RBrack -> "]";
-      Comma -> ","; Dot -> "."; Or -> "|"; And -> "&"; Not -> "~";
-      Iff -> "<=>"; Implies -> "=>"; Follows -> "<="; Xor -> "<~>";
-      Nor -> "~|"; Nand -> "~&"; Eq -> "="; Neq -> "!="; ForAll -> "!";
-      Exists -> "?"; Let -> ":="; Colon -> ":"; Times -> "*"; Plus -> "+";
-      FunArrow -> ">"; Lambda -> "^"; Apply -> "@"; ForAllLam -> "!!";
-      ExistsLam -> "??"; Some -> "@+"; The -> "@-"; Subtype -> "<<";
-      SequentArrow -> "-->"; DependentProduct -> "!>"; DependentSum -> "?*";
-      LetTerm -> ":-" }
+  show = unintern . showPunct
 
 p x = const (Punct x)
 k x = Atom x . copy
 d x = const (Defined x)
 
-copy :: String -> String
-copy = id
+copy :: String -> Symbol
+copy = intern
 
 unquote :: String -> String
 unquote (_:x)
diff --git a/src/Jukebox/TPTP/Parse/Core.hs b/src/Jukebox/TPTP/Parse/Core.hs
--- a/src/Jukebox/TPTP/Parse/Core.hs
+++ b/src/Jukebox/TPTP/Parse/Core.hs
@@ -20,7 +20,7 @@
 
 import Jukebox.TPTP.Lexer hiding
   (Pos, Error, Include, Var, Type, Not, ForAll,
-   Exists, And, Or, Type, Apply, Implies, Follows, Xor, Nand, Nor,
+   Exists, And, Or, Type, Implies, Follows, Xor, Nand, Nor,
    Rational, Real, NegatedConjecture, Question,
    Axiom, Hypothesis, Definition, Assumption, Lemma, Theorem, NegatedConjecture,
    Conjecture, Question,
@@ -35,9 +35,9 @@
 data ParseState =
   MkState (Maybe String)           -- filename
           ![Input Form]            -- problem being constructed, inputs are in reverse order
-          !(Map String Type)       -- types in scope
-          !(Map String [Function]) -- functions in scope
-          !(Map String Variable)   -- variables in scope, for CNF
+          !(Map Symbol Type)       -- types in scope
+          !(Map Symbol [Function]) -- functions in scope
+          !(Map Symbol Variable)   -- variables in scope, for CNF
           !Int64                   -- unique supply
 type Parser = Parsec ParsecState
 type ParsecState = UserState ParseState TokenStream
@@ -49,9 +49,9 @@
 initialState :: Maybe String -> ParseState
 initialState mfile =
   initialStateFrom mfile []
-    (Map.fromList [(show (name ty), ty) | ty <- [intType, ratType, realType]])
+    (Map.fromList [(intern (show (name ty)), ty) | ty <- [intType, ratType, realType]])
     (Map.fromList
-       [ (fun,
+       [ (intern fun,
           [Fixed (Overloaded (intern fun) (intern (show (name kind)))) Nothing ::: ty
           | (kind, ty) <- tys ])
        | (fun, tys) <- funs ])
@@ -76,7 +76,7 @@
        fun ["$to_rat"]  (\ty -> FunType [ty] ratType) ++
        fun ["$to_real"] (\ty -> FunType [ty] realType)
 
-initialStateFrom :: Maybe String -> [Name] -> Map String Type -> Map String [Function] -> ParseState
+initialStateFrom :: Maybe String -> [Name] -> Map Symbol Type -> Map Symbol [Function] -> ParseState
 initialStateFrom mfile xs tys fs = MkState mfile [] tys fs Map.empty n
   where
     n = maximum (0:[succ m | Unique m _ _ _ <- xs])
@@ -174,6 +174,16 @@
         p' _ = False
 {-# INLINE punct #-}
 punct k = punct' (== k) <?> "'" ++ show k ++ "'"
+{-# INLINE operator #-}
+operator = punct' p <?> "operator"
+  where
+    p Dot = True
+    p Colon = True
+    p Times = True
+    p Plus = True
+    p FunArrow = True
+    p (Other _) = True
+    p _ = False
 {-# INLINE defined' #-}
 defined' p = fmap L.defined (satisfy p')
   where p' Defined { L.defined = d } = p d
@@ -277,7 +287,7 @@
 
 -- A formula name.
 tag :: Parser Tag
-tag = atom <|> fmap show number <?> "clause name"
+tag = fmap unintern atom <|> fmap show number <?> "clause name"
 
 -- An include declaration.
 include :: Parser IncludeStatement
@@ -287,7 +297,7 @@
     name <- atom <?> "quoted filename"
     clauses <- do { punct Comma
                   ; fmap Just (bracks (sepBy1 tag (punct Comma))) } <|> return Nothing
-    return (Include name clauses)
+    return (Include (unintern name) clauses)
   punct Dot
   return res
 
@@ -298,12 +308,12 @@
   MkState mfile p t f v n <- getState
   putState (MkState mfile (input:p) t f v n)
   
-newFunction :: String -> FunType -> Parser Function
+newFunction :: Symbol -> FunType -> Parser Function
 newFunction name ty = do
   fs <- lookupFunction ty name
   case [ f | f <- fs, rhs f == ty ] of
     [] ->
-      fatalError $ "Constant " ++ name ++
+      fatalError $ "Constant " ++ unintern name ++
                    " was declared to have type " ++ prettyShow ty ++
                    " but already has type " ++ showTypes (map rhs fs)
     (f:_) -> return f
@@ -312,7 +322,7 @@
 showTypes = intercalate " and " . map prettyShow
 
 {-# INLINE applyFunction #-}
-applyFunction :: String -> [Term] -> Type -> Parser Term
+applyFunction :: Symbol -> [Term] -> Type -> Parser Term
 applyFunction name args res = do
   fs <- lookupFunction (FunType (replicate (length args) indType) res) name
   case [ f | f <- fs, funArgs f == map typ args ] of
@@ -336,7 +346,7 @@
                    " of type " ++ intercalate ", " (map (prettyShow . typ) args')
 
 {-# INLINE lookupType #-}
-lookupType :: String -> Parser Type
+lookupType :: Symbol -> Parser Type
 lookupType xs = do
   MkState mfile p t f v n <- getState
   case Map.lookup xs t of
@@ -347,7 +357,7 @@
     Just ty -> return ty
 
 {-# INLINE lookupFunction #-}
-lookupFunction :: FunType -> String -> Parser [Name ::: FunType]
+lookupFunction :: FunType -> Symbol -> Parser [Name ::: FunType]
 lookupFunction def x = do
   MkState mfile p t f v n <- getState
   case Map.lookup x f of
@@ -376,14 +386,14 @@
 -- A thing is either a term or a formula, or a literal that we don't know
 -- if it should be a term or a formula. Instead of a separate formula-parser
 -- and term-parser we have a combined thing-parser.
-data Thing = Apply !String ![Term]
+data Thing = Apply !Symbol ![Term]
            | Term !Term
            | Formula !Form
 
 instance Show Thing where
-  show (Apply f []) = f
+  show (Apply f []) = unintern f
   show (Apply f args) =
-    f ++
+    unintern f ++
       case args of
         [] -> ""
         args -> prettyShow args
@@ -395,7 +405,7 @@
 -- the error messages are better). For that reason, our parser is
 -- parametrised on the type of thing you want to parse. We have two
 -- main parsers:
---   * 'term' parses an atomic expression
+--   * 'term' parses a term or predicate
 --   * 'formula' parses an arbitrary expression
 -- You can instantiate 'term' for Term, Form or Thing; in each case
 -- you get an appropriate parser. You can instantiate 'formula' for
@@ -407,9 +417,11 @@
   -- Convert from a Thing.
   fromThing :: Thing -> Parser a
   -- Parse a variable occurrence as a term on its own, if that's allowed.
-  var :: Mode -> Map String Variable -> Parser a
+  var :: Mode -> Map Symbol Variable -> Parser a
+  -- Parse the input as a formula, if that's allowed.
+  parseFormula :: Parser Form -> Parser a
   -- A parser for this type.
-  parser :: Mode -> Map String Variable -> Parser a
+  parser :: Mode -> Map Symbol Variable -> Parser a
 
 data Mode = Typed | Untyped | NoQuantification
 
@@ -420,6 +432,7 @@
   fromThing (Formula f) = return f
   -- A variable itself is not a valid formula.
   var _ _ = mzero
+  parseFormula = id
   parser = formula
 
 instance TermLike Term where
@@ -427,6 +440,7 @@
   fromThing (Apply x xs) = applyFunction x xs indType
   fromThing (Term t) = return t
   fromThing (Formula _) = mzero
+  parseFormula _ = mzero
   parser = term
 
   {-# INLINE var #-}
@@ -443,25 +457,18 @@
     x <- variable
     case Map.lookup x ctx of
       Just v -> return (Var v)
-      Nothing -> fatalError $ "unbound variable " ++ x
+      Nothing -> fatalError $ "unbound variable " ++ unintern x
 
 instance TermLike Thing where
   fromThing = return
   var mode ctx = fmap Term (var mode ctx)
+  parseFormula = fmap Formula
   parser = formula
 
--- Types that can represent formulae. These are the types on which
--- you can use 'formula'.
-class TermLike a => FormulaLike a where
-  fromFormula :: Form -> a
-
-instance FormulaLike Form where fromFormula = id
-instance FormulaLike Thing where fromFormula = Formula
-
 -- An atomic expression.
-{-# INLINEABLE term #-}
-term :: TermLike a => Mode -> Map String Variable -> Parser a
-term mode ctx = function <|> var mode ctx <|> num <|> parens (parser mode ctx)
+{-# INLINEABLE atomic #-}
+atomic :: TermLike a => Mode -> Map Symbol Variable -> Parser a
+atomic mode ctx = function <|> var mode ctx <|> num <|> parens (parser mode ctx)
   where
     {-# INLINE function #-}
     function = do
@@ -491,18 +498,36 @@
     constant x ty =
       fromThing (Term ((Fixed x Nothing ::: FunType [] ty) :@: []))
 
+unary :: TermLike a => Mode -> Map Symbol Variable -> Parser a
+unary mode ctx =
+  atomic mode ctx <|> do
+    Punct p <- operator
+    arg <- atomic mode ctx :: Parser Term
+    fromThing (Apply (showPunct p) [arg])
+
+term :: TermLike a => Mode -> Map Symbol Variable -> Parser a
+term mode ctx = do
+  t <- unary mode ctx :: Parser Thing
+  let
+    binop = do
+      Punct p <- operator
+      lhs <- fromThing t :: Parser Term
+      rhs <- unary mode ctx :: Parser Term
+      fromThing (Apply (showPunct p) [lhs, rhs])
+  binop <|> fromThing t
+
 literal, unitary, quantified, formula ::
-  FormulaLike a => Mode -> Map String Variable -> Parser a
+  TermLike a => Mode -> Map Symbol Variable -> Parser a
 {-# INLINE literal #-}
 literal mode ctx = true <|> false <|> binary <?> "literal"
   where {-# INLINE true #-}
-        true = do { defined DTrue; return (fromFormula (And [])) }
+        true = parseFormula $ do { defined DTrue; return (And []) }
         {-# INLINE false #-}
-        false = do { defined DFalse; return (fromFormula (Or [])) }
+        false = parseFormula $ do { defined DFalse; return (Or []) }
         binary = do
           x <- term mode ctx :: Parser Thing
           let {-# INLINE f #-}
-              f p sign = do
+              f p sign = parseFormula $ do
                punct p
                lhs <- fromThing x :: Parser Term
                rhs <- term mode ctx :: Parser Term
@@ -514,25 +539,25 @@
                when (typ lhs == O) $
                  fatalError $ "Type error in equality '" ++ prettyShow (prettyNames form) ++
                  "': can't use equality on predicate (use <=> or <~> instead)"
-               return (fromFormula form)
+               return form
           f Eq Pos <|> f Neq Neg <|> fromThing x
 
 {-# INLINEABLE unitary #-}
 unitary mode ctx = negation <|> quantified mode ctx <|> literal mode ctx
   where {-# INLINE negation #-}
-        negation = do
+        negation = parseFormula $ do
           punct L.Not
-          fmap (fromFormula . Not) (unitary mode ctx :: Parser Form)
+          fmap Not $ unitary mode ctx
 
 {-# INLINE quantified #-}
-quantified mode ctx = do
+quantified mode ctx = parseFormula $ do
   q <- (punct L.ForAll >> return ForAll) <|>
        (punct L.Exists >> return Exists)
   vars <- bracks (sepBy1 (binder mode) (punct Comma))
-  let ctx' = foldl' (\m v -> Map.insert (Name.base (Name.name v)) v m) ctx vars
+  let ctx' = foldl' (\m v -> Map.insert (intern (Name.base (Name.name v))) v m) ctx vars
   punct Colon
   rest <- unitary mode ctx' :: Parser Form
-  return (fromFormula (q (Bind (Set.fromList vars) rest)))
+  return (q (Bind (Set.fromList vars) rest))
 
 -- A general formula.
 {-# INLINEABLE formula #-}
@@ -540,11 +565,11 @@
   x <- unitary mode ctx :: Parser Thing
   let binop op t u = op [t, u]
       {-# INLINE connective #-}
-      connective p op = do
+      connective p op = parseFormula $ do
         punct p
         lhs <- fromThing x
         rhs <- formula mode ctx :: Parser Form
-        return (fromFormula (op lhs rhs))
+        return (op lhs rhs)
   connective L.And (binop And) <|> connective L.Or (binop Or) <|>
    connective Iff Equiv <|>
    connective L.Implies (Connective Implies) <|>
diff --git a/src/Jukebox/TPTP/ParseSnippet.hs b/src/Jukebox/TPTP/ParseSnippet.hs
--- a/src/Jukebox/TPTP/ParseSnippet.hs
+++ b/src/Jukebox/TPTP/ParseSnippet.hs
@@ -1,6 +1,6 @@
 -- Parse little bits of TPTP, e.g. a prelude for a particular tool.
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, OverloadedStrings #-}
 module Jukebox.TPTP.ParseSnippet where
 
 import Jukebox.TPTP.Parse.Core as TPTP.Parse.Core
@@ -13,41 +13,43 @@
 #if __GLASGOW_HASKELL__ < 710
 import Control.Applicative
 #endif
+import Data.Symbol
 
 tff, cnf :: [(String, Type)] -> [(String, Function)] -> String -> Form
 tff = form TPTP.Parse.Core.tff
 cnf = form TPTP.Parse.Core.cnf
 
 form :: Symbolic a => Parser a -> [(String, Type)] -> [(String, Function)] -> String -> a
-form parser types funs0 str =
+form parser types0 funs0 str =
   case run_ (parser <* eof)
-            (UserState (MkState Nothing [] (Map.delete "$i" (Map.fromList types)) (Map.fromList funs) Map.empty 0) (scan str)) of
+            (UserState (MkState Nothing [] (Map.delete "$i" types) funs Map.empty 0) (scan str)) of
     Ok (UserState (MkState _ _ types' funs' _ _) (At _ (Cons Eof _))) res
-      | Map.insert "$i" indType (Map.fromList types) /=
+      | Map.insert "$i" indType types /=
         Map.insert "$i" indType types' ->
         error $ "ParseSnippet: type implicitly defined: " ++
-                show (map snd (Map.toList types' \\ types))
-      | Map.fromList funs /= funs' ->
+                show (map snd (Map.toList types' \\ Map.toList types))
+      | funs /= funs' ->
         error $ "ParseSnippet: function implicitly defined: " ++
-                show (map snd (Map.toList funs' \\ funs))
+                show (map snd (Map.toList funs' \\ Map.toList funs))
       | otherwise -> mapType elimI res
     Ok{} -> error "ParseSnippet: lexical error"
     TPTP.Parsec.Error _ msg -> error $ "ParseSnippet: parse error: " ++ msg
     Expected _ exp -> error $ "ParseSnippet: parse error: expected " ++ show exp
 
   where
-    funs = map (mapFunType introI) funs0
+    funs = Map.mapKeys intern $ Map.fromList $ map (mapFunType introI) funs0
+    types = Map.mapKeys intern $ Map.fromList types0
 
     mapFunType f (xs, name ::: FunType args res) =
       (xs, [name ::: FunType (map f args) (f res)])
 
     elimI =
-      case lookup "$i" types of
+      case Map.lookup "$i" types of
         Nothing -> id
         Just i ->
           \ty -> if ty == indType then i else ty
     introI =
-      case lookup "$i" types of
+      case Map.lookup "$i" types of
         Nothing -> id
         Just i ->
           \ty -> if ty == i then indType else ty
diff --git a/src/Jukebox/TPTP/Print.hs b/src/Jukebox/TPTP/Print.hs
--- a/src/Jukebox/TPTP/Print.hs
+++ b/src/Jukebox/TPTP/Print.hs
@@ -18,6 +18,7 @@
 import Jukebox.Utils
 import Text.PrettyPrint.HughesPJClass
 import Control.Monad.Trans.State.Strict
+import Data.Symbol
 
 pPrintClauses :: Problem Clause -> Doc
 pPrintClauses prob0
@@ -204,10 +205,10 @@
   pPrint = text . show
 
 instance Show L.Token where
-  show L.Atom{L.tokenName = x} = escapeAtom x
+  show L.Atom{L.tokenName = x} = escapeAtom (unintern x)
   show L.Defined{L.defined = x} = show x
-  show L.Var{L.tokenName = x} = x
-  show L.DistinctObject{L.tokenName = x} = quote '"' x
+  show L.Var{L.tokenName = x} = unintern x
+  show L.DistinctObject{L.tokenName = x} = quote '"' (unintern x)
   show L.Number{L.value = x} = show x
   show L.Punct{L.kind = x} = show x
   show L.Eof = "end of file"
@@ -340,7 +341,7 @@
     add1 (Fixed xs _) (scope, used) =
       (scope, Set.insert (show xs) used)
     add1 x@(Unique _ base _ f) (scope, used) =
-      addWith base f x (scope, used)
+      addWith (unintern base) f x (scope, used)
     add1 x@(Variant y _ f) (scope, used) =
       addWith (base y) f x (scope, used)
 
diff --git a/src/Jukebox/Toolbox.hs b/src/Jukebox/Toolbox.hs
--- a/src/Jukebox/Toolbox.hs
+++ b/src/Jukebox/Toolbox.hs
@@ -93,10 +93,6 @@
 forAllFilesBox = forAllFiles <$> filenames
 
 forAllFiles :: [FilePath] -> (FilePath -> IO ()) -> IO ()
-forAllFiles [] _ = do
-  hPutStrLn stderr "No input files specified! Try --help."
-  hPutStrLn stderr "You can use \"-\" to read from standard input."
-  exitWith (ExitFailure 1)
 forAllFiles xs f = mapM_ f xs
 
 ----------------------------------------------------------------------