src/HOL/Tools/ATP/atp_proof_reconstruct.ML

 val have_prefix = "f"
 
 fun raw_label_for_name (num, ss) =
   case resolve_conjecture ss of
     [j] => (conjecture_prefix, j)
-  | _ => case Int.fromString num of
-           SOME j => (raw_prefix, j)
-         | NONE => (raw_prefix ^ num, 0)
+  | _ => (raw_prefix ^ ascii_of num, 0)
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
 
 exception HO_TERM of (string, string) ho_term list
 exception FORMULA of (string, string, (string, string) ho_term) formula list

         step :: aux subst depth nextp proof
   in aux [] 0 (1, 1) end
 
 fun string_for_proof ctxt0 type_enc lam_trans i n =
   let
-    val ctxt =
-      ctxt0 |> Config.put show_free_types false
-            |> Config.put show_types true
-            |> Config.put show_sorts true
+    val ctxt = ctxt0
+(* FIXME: Implement proper handling of type constraints:
+      |> Config.put show_free_types false
+      |> Config.put show_types false
+      |> Config.put show_sorts false
+*)
     fun fix_print_mode f x =
       Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
                                (print_mode_value ())) f x
     fun do_indent ind = replicate_string (ind * indent_size) " "
     fun do_free (s, T) =

                             |> member (op = o apsnd fst) tainted s ? s_not))
                   atp_proof
         fun prop_of_clause c =
           fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
                @{term False}
-        fun label_of_clause c = (space_implode "___" (map fst c), 0)
+        fun label_of_clause [name] = raw_label_for_name name
+          | label_of_clause c = (space_implode "___" (map fst c), 0)
         fun maybe_show outer c =
           (outer andalso length c = 1 andalso subset (op =) (c, conjs))
           ? cons Show
         fun do_have outer qs (gamma, c) =
           Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c,