diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.3.5
+Version: 0.3.6
 Cabal-version: >= 1.8
 Build-type: Simple
 Author: Nick Smallbone
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
@@ -99,7 +99,7 @@
 tags :: Bool -> Scheme
 tags moreAxioms = Scheme
   { makeFunction = \ty ->
-      newFunction ("$to_" ++ base ty) [ty] ty,
+      newFunction ("$$to_" ++ base ty) [ty] ty,
     scheme1 = tags1 moreAxioms }
 
 tags1 :: Bool -> (Type -> Bool) -> (Type -> Function) -> Scheme1
@@ -147,7 +147,7 @@
 guards :: Scheme
 guards = Scheme
   { makeFunction = \ty ->
-      newFunction ("$is_" ++ base ty) [ty] O,
+      newFunction ("$$is_" ++ base ty) [ty] O,
     scheme1 = guards1 }
 
 guards1 :: (Type -> Bool) -> (Type -> Function) -> Scheme1
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
@@ -116,8 +116,8 @@
       ((p ::: FunType tys bool) :@: ts) :=: true
 
     (bool, true) = run_ prob $ do
-      bool <- newType "bool"
-      true <- newFunction "true" [] bool
+      bool <- newType "$$bool"
+      true <- newFunction "$$true" [] bool
       return (bool, true :@: [])
 
 eliminateMultiplePreconditions :: HornFlags -> Problem Clause -> Problem Clause
@@ -166,9 +166,9 @@
     addConjecture c = clause (Pos (a :=: b):toLiterals c)
 
     (a, b) = run_ prob $ do
-      token <- newType "$token"
-      a <- newFunction "$a" [] token
-      b <- newFunction "$b" [] token
+      token <- newType "$$token"
+      a <- newFunction "$$a" [] token
+      b <- newFunction "$$b" [] token
       return (a :@: [], b :@: [])
 
 eliminateHornClauses :: HornFlags -> Problem Clause -> Either (Input Clause) (Problem Clause)
@@ -286,8 +286,8 @@
         what = clause [Pos l] }
 
     (ifeqName, passiveName, xvar, yvar, zvar) = run_ prob $ do
-      ifeqName <- newName "$ifeq"
-      passiveName <- newName "$passive"
+      ifeqName <- newName "$$ifeq"
+      passiveName <- newName "$$passive"
       xvar <- newName "A"
       yvar <- newName "B"
       zvar <- newName "C"