1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 15 11:26:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 15 11:26:28 2010 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4      bool -> int -> (string * string) list -> (failure * string) list -> string
     1.5      -> string * failure option
     1.6    val is_same_step : step_name * step_name -> bool
     1.7 -  val atp_proof_from_tstplike_string : string -> string proof
     1.8 +  val atp_proof_from_tstplike_string : bool -> string -> string proof
     1.9    val map_term_names_in_atp_proof :
    1.10      (string -> string) -> string proof -> string proof
    1.11    val nasty_atp_proof : string Symtab.table -> string proof -> string proof
    1.12 @@ -280,9 +280,14 @@
    1.13  
    1.14  (**** PARSING OF VAMPIRE OUTPUT ****)
    1.15  
    1.16 +val parse_vampire_braced_stuff =
    1.17 +  $$ "{" -- scan_general_id -- $$ "}"
    1.18 +  -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
    1.19 +
    1.20  (* Syntax: <num>. <formula> <annotation> *)
    1.21  val parse_vampire_line =
    1.22 -  scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
    1.23 +  scan_general_id --| $$ "." -- parse_formula
    1.24 +    --| Scan.option parse_vampire_braced_stuff -- parse_annotation true
    1.25    >> (fn ((num, phi), deps) =>
    1.26           Inference ((num, NONE), phi, map (rpair NONE) deps))
    1.27  
    1.28 @@ -337,11 +342,11 @@
    1.29      Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
    1.30      clean_up_dependencies (name :: seen) steps
    1.31  
    1.32 -val atp_proof_from_tstplike_string =
    1.33 +fun atp_proof_from_tstplike_string clean =
    1.34    suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
    1.35    #> parse_proof
    1.36 -  #> sort (step_name_ord o pairself step_name)
    1.37 -  #> clean_up_dependencies []
    1.38 +  #> clean ? (sort (step_name_ord o pairself step_name)
    1.39 +              #> clean_up_dependencies [])
    1.40  
    1.41  fun map_term_names_in_term f (ATerm (s, ts)) =
    1.42    ATerm (f s, map (map_term_names_in_term f) ts)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
     2.3 @@ -161,7 +161,8 @@
     2.4    | add_fact _ _ = I
     2.5  
     2.6  fun used_facts_in_tstplike_proof fact_names =
     2.7 -  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
     2.8 +  atp_proof_from_tstplike_string false
     2.9 +  #> rpair [] #-> fold (add_fact fact_names)
    2.10  
    2.11  val split_used_facts =
    2.12    List.partition (curry (op =) Chained o snd)
    2.13 @@ -608,7 +609,7 @@
    2.14    let
    2.15      val lines =
    2.16        tstplike_proof
    2.17 -      |> atp_proof_from_tstplike_string
    2.18 +      |> atp_proof_from_tstplike_string true
    2.19        |> nasty_atp_proof pool
    2.20        |> map_term_names_in_atp_proof repair_name
    2.21        |> decode_lines ctxt type_sys tfrees