1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 16:54:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 17:38:40 2010 +0200
     1.3 @@ -401,11 +401,6 @@
     1.4         class_rel_clauses, arity_clauses))
     1.5    end
     1.6  
     1.7 -val axiom_prefix = "ax_"
     1.8 -val conjecture_prefix = "conj_"
     1.9 -val arity_clause_prefix = "clsarity_"
    1.10 -val tfrees_name = "tfrees"
    1.11 -
    1.12  fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
    1.13  
    1.14  fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 16:54:12 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Jul 28 17:38:40 2010 +0200
     2.3 @@ -10,6 +10,10 @@
     2.4  sig
     2.5    type minimize_command = string list -> string
     2.6  
     2.7 +  val axiom_prefix : string
     2.8 +  val conjecture_prefix : string
     2.9 +  val arity_clause_prefix : string
    2.10 +  val tfrees_name : string
    2.11    val metis_line: bool -> int -> int -> string list -> string
    2.12    val metis_proof_text:
    2.13      bool * minimize_command * string * string vector * thm * int
    2.14 @@ -34,6 +38,11 @@
    2.15  
    2.16  type minimize_command = string list -> string
    2.17  
    2.18 +val axiom_prefix = "ax_"
    2.19 +val conjecture_prefix = "conj_"
    2.20 +val arity_clause_prefix = "clsarity_"
    2.21 +val tfrees_name = "tfrees"
    2.22 +
    2.23  (* Simple simplifications to ensure that sort annotations don't leave a trail of
    2.24     spurious "True"s. *)
    2.25  fun s_not @{const False} = @{const True}
    2.26 @@ -548,15 +557,28 @@
    2.27     (108) is extracted. For SPASS, lines have the form "108[0:Inp] ...", where
    2.28     the first number (108) is extracted. For Vampire, we look for
    2.29     "108. ... [input]". *)
    2.30 -fun extract_formula_numbers_in_atp_proof atp_proof =
    2.31 +fun used_facts_in_atp_proof thm_names atp_proof =
    2.32    let
    2.33 -    val tokens_of = String.tokens (not o Char.isAlphaNum)
    2.34 -    fun extract_num ("fof" :: num :: "axiom" :: _) = Int.fromString num
    2.35 -      | extract_num (num :: "0" :: "Inp" :: _) = Int.fromString num
    2.36 -      | extract_num (num :: rest) =
    2.37 -        (case List.last rest of "input" => Int.fromString num | _ => NONE)
    2.38 -      | extract_num _ = NONE
    2.39 -  in atp_proof |> split_lines |> map_filter (extract_num o tokens_of) end
    2.40 +    fun axiom_name num =
    2.41 +      let val j = Int.fromString num |> the_default ~1 in
    2.42 +        if is_axiom_clause_number thm_names j then
    2.43 +          SOME (Vector.sub (thm_names, j - 1))
    2.44 +        else
    2.45 +          NONE
    2.46 +      end
    2.47 +    val tokens_of =
    2.48 +      String.tokens (fn c => not (Char.isAlphaNum c) andalso c <> #"_")
    2.49 +    val thm_name_list = Vector.foldr (op ::) [] thm_names
    2.50 +    fun do_line ("fof" :: num :: "axiom" :: (rest as _ :: _)) =
    2.51 +        (case strip_prefix_and_undo_ascii axiom_prefix (List.last rest) of
    2.52 +           SOME name =>
    2.53 +           if member (op =) rest "file" then SOME name else axiom_name num
    2.54 +         | NONE => axiom_name num)
    2.55 +      | do_line (num :: "0" :: "Inp" :: _) = axiom_name num
    2.56 +      | do_line (num :: rest) =
    2.57 +        (case List.last rest of "input" => axiom_name num | _ => NONE)
    2.58 +      | do_line _ = NONE
    2.59 +  in atp_proof |> split_lines |> map_filter (do_line o tokens_of) end
    2.60  
    2.61  val indent_size = 2
    2.62  val no_label = ("", ~1)
    2.63 @@ -593,9 +615,7 @@
    2.64  val unprefix_chained = perhaps (try (unprefix chained_prefix))
    2.65  
    2.66  fun used_facts thm_names =
    2.67 -  extract_formula_numbers_in_atp_proof
    2.68 -  #> filter (is_axiom_clause_number thm_names)
    2.69 -  #> map (fn i => Vector.sub (thm_names, i - 1))
    2.70 +  used_facts_in_atp_proof thm_names
    2.71    #> List.partition (String.isPrefix chained_prefix)
    2.72    #>> map (unprefix chained_prefix)
    2.73    #> pairself (sort_distinct string_ord)