1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon May 14 15:54:26 2012 +0200
     1.3 @@ -299,9 +299,7 @@
     1.4  fun raw_label_for_name (num, ss) =
     1.5    case resolve_conjecture ss of
     1.6      [j] => (conjecture_prefix, j)
     1.7 -  | _ => case Int.fromString num of
     1.8 -           SOME j => (raw_prefix, j)
     1.9 -         | NONE => (raw_prefix ^ num, 0)
    1.10 +  | _ => (raw_prefix ^ ascii_of num, 0)
    1.11  
    1.12  (**** INTERPRETATION OF TSTP SYNTAX TREES ****)
    1.13  
    1.14 @@ -797,10 +795,12 @@
    1.15  
    1.16  fun string_for_proof ctxt0 type_enc lam_trans i n =
    1.17    let
    1.18 -    val ctxt =
    1.19 -      ctxt0 |> Config.put show_free_types false
    1.20 -            |> Config.put show_types true
    1.21 -            |> Config.put show_sorts true
    1.22 +    val ctxt = ctxt0
    1.23 +(* FIXME: Implement proper handling of type constraints:
    1.24 +      |> Config.put show_free_types false
    1.25 +      |> Config.put show_types false
    1.26 +      |> Config.put show_sorts false
    1.27 +*)
    1.28      fun fix_print_mode f x =
    1.29        Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    1.30                                 (print_mode_value ())) f x
    1.31 @@ -903,7 +903,8 @@
    1.32          fun prop_of_clause c =
    1.33            fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c)
    1.34                 @{term False}
    1.35 -        fun label_of_clause c = (space_implode "___" (map fst c), 0)
    1.36 +        fun label_of_clause [name] = raw_label_for_name name
    1.37 +          | label_of_clause c = (space_implode "___" (map fst c), 0)
    1.38          fun maybe_show outer c =
    1.39            (outer andalso length c = 1 andalso subset (op =) (c, conjs))
    1.40            ? cons Show