diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.2
+Version: 0.5.3
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
diff --git a/src/Jukebox/Form.hs b/src/Jukebox/Form.hs
--- a/src/Jukebox/Form.hs
+++ b/src/Jukebox/Form.hs
@@ -105,6 +105,26 @@
 size Var{} = 1
 size (_f :@: xs) = 1 + sum (map size xs)
 
+subterms :: Term -> [Term]
+subterms t =
+  t:
+  case t of
+    Var _ -> []
+    _f :@: ts -> concatMap subterms ts
+
+contexts :: Term -> [(Term, Term -> Term)]
+contexts t = ctxs t id
+  where
+    ctxs :: Term -> (Term -> Term) -> [(Term, Term -> Term)]
+    ctxs t k =
+      (t, k):
+      case t of
+        Var _ -> []
+        f :@: ts ->
+          concat
+          [ ctxs (ts !! i) (\u -> k (f :@: (take i ts ++ [u] ++ drop (i+1) ts)))
+          | i <- [0..length ts-1] ]
+
 ----------------------------------------------------------------------
 -- Literals
 
@@ -519,6 +539,19 @@
 
     generic :: Symbolic a => a -> a
     generic t = recursively (subst s) t
+
+match :: Term -> Term -> Maybe Subst
+match pat t = execStateT (matchM pat t) ids
+  where
+    matchM (Var x) t = do
+      sub <- get
+      case Map.lookup x sub of
+        Nothing -> put (sub |+| (x |=> t))
+        Just u | u == t -> return ()
+        _ -> mzero
+    matchM (f :@: ts) (g :@: us) | f == g =
+      zipWithM_ matchM ts us
+    matchM _ _ = mzero
 
 ----------------------------------------------------------------------
 -- Functions operating on symbolic terms
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
@@ -56,7 +56,7 @@
           | (kind, ty) <- tys ])
        | (fun, tys) <- funs ])
    where
-     overloads f = [(ty, f ty) | ty <- [intType, ratType, realType]]
+     overloads f = [(ty, f ty) | ty <- [intType, ratType, realType, indType]]
      fun xs f = [(x, overloads f) | x <- xs]
 
      funs =
diff --git a/src/Jukebox/Tools/EncodeTypes.hs b/src/Jukebox/Tools/EncodeTypes.hs
--- a/src/Jukebox/Tools/EncodeTypes.hs
+++ b/src/Jukebox/Tools/EncodeTypes.hs
@@ -82,7 +82,17 @@
                 fmap notInwards $ prepare $ nt f
       trType O = O
       trType _ = indType
-  in Form.run (translate1 scheme mono f') (return . mapType trType)
+      quoteNumbers tagName name
+        | isNumber name = name `variant` [tagName]
+        | otherwise = name
+      isNumber (Fixed (Integer _) _) = True
+      isNumber (Fixed (Rational _) _) = True
+      isNumber (Fixed (Real _) _) = True
+      isNumber _ = False
+
+  in Form.run (translate1 scheme mono f') $ \form -> do
+    name <- newName ""
+    return $ mapName (quoteNumbers name) $ mapType trType form
 
 -- Typing functions.