src/HOL/Tools/ATP/atp_proof.ML

     (failure * string) list -> string -> failure option
   val extract_tstplike_proof_and_outcome :
     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
 end;
 

             | _ => Inference (name, phi, map (rpair NONE) deps)
           end)
 
 (**** 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))
 
 (**** PARSING OF SPASS OUTPUT ****)
 

     step :: clean_up_dependencies (name :: seen) steps
   | clean_up_dependencies seen (Inference (name, u, deps) :: steps) =
     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)
 fun map_term_names_in_formula f (AQuant (q, xs, phi)) =
     AQuant (q, xs, map_term_names_in_formula f phi)