diff --git a/jukebox.cabal b/jukebox.cabal
--- a/jukebox.cabal
+++ b/jukebox.cabal
@@ -1,5 +1,5 @@
 Name: jukebox
-Version: 0.5.6
+Version: 0.5.7
 Cabal-version: >= 1.10
 Build-type: Simple
 Author: Nick Smallbone
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
@@ -123,7 +123,7 @@
 pPrintAnnotProof annots0 =
   vcat $
     [ vcat (pPrintDecls "tff" inps) | not (isReallyFof inps) ] ++
-    [ pPrintClause (family x) (tag inp) k (pp x:rest) <+> text (show (ident inp))
+    [ pPrintClause (family x) (tag inp) k (pp x:rest)
     | (inp, (k, rest)) <- annots,
       let x = what inp ]
   where