# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID be78f4053bce0c5e965041721ec0a1597c69319d
# Parent  a5ee3b8e5a90113f1d3ff08936d35d1ffc7af145
fix Vampire parsing problem

diff -r a5ee3b8e5a90 -r be78f4053bce src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -34,7 +34,7 @@
     bool -> int -> (string * string) list -> (failure * string) list -> string
     -> string * failure option
   val is_same_step : step_name * step_name -> bool
-  val atp_proof_from_tstplike_string : string -> string proof
+  val atp_proof_from_tstplike_string : bool -> string -> string proof
   val map_term_names_in_atp_proof :
     (string -> string) -> string proof -> string proof
   val nasty_atp_proof : string Symtab.table -> string proof -> string proof
@@ -280,9 +280,14 @@
 
 (**** PARSING OF VAMPIRE OUTPUT ****)
 
+val parse_vampire_braced_stuff =
+  $$ "{" -- scan_general_id -- $$ "}"
+  -- Scan.option ($$ "(" |-- parse_vampire_detritus --| $$ ")")
+
 (* Syntax: <num>. <formula> <annotation> *)
 val parse_vampire_line =
-  scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
+  scan_general_id --| $$ "." -- parse_formula
+    --| Scan.option parse_vampire_braced_stuff -- parse_annotation true
   >> (fn ((num, phi), deps) =>
          Inference ((num, NONE), phi, map (rpair NONE) deps))
 
@@ -337,11 +342,11 @@
     Inference (name, u, map_filter (clean_up_dependency seen) deps) ::
     clean_up_dependencies (name :: seen) steps
 
-val atp_proof_from_tstplike_string =
+fun atp_proof_from_tstplike_string clean =
   suffix "$" (* the $ sign acts as a sentinel (FIXME: needed?) *)
   #> parse_proof
-  #> sort (step_name_ord o pairself step_name)
-  #> clean_up_dependencies []
+  #> clean ? (sort (step_name_ord o pairself step_name)
+              #> clean_up_dependencies [])
 
 fun map_term_names_in_term f (ATerm (s, ts)) =
   ATerm (f s, map (map_term_names_in_term f) ts)
diff -r a5ee3b8e5a90 -r be78f4053bce src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -161,7 +161,8 @@
   | add_fact _ _ = I
 
 fun used_facts_in_tstplike_proof fact_names =
-  atp_proof_from_tstplike_string #> rpair [] #-> fold (add_fact fact_names)
+  atp_proof_from_tstplike_string false
+  #> rpair [] #-> fold (add_fact fact_names)
 
 val split_used_facts =
   List.partition (curry (op =) Chained o snd)
@@ -608,7 +609,7 @@
   let
     val lines =
       tstplike_proof
-      |> atp_proof_from_tstplike_string
+      |> atp_proof_from_tstplike_string true
       |> nasty_atp_proof pool
       |> map_term_names_in_atp_proof repair_name
       |> decode_lines ctxt type_sys tfrees