Multiple subgoals working.

--- a/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 17 16:12:49 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 17 16:18:49 2005 +0200
@@ -135,8 +135,20 @@
 \\
 \--------------------------SPASS-STOP------------------------------"
 
+fun extract_proof s
+      = if cut_exists "Here is a proof with" s then
+          (kill_lines 0
+           o snd o cut_after ":"
+           o snd o cut_after "Here is a proof with"
+           o fst o cut_after " ||  -> .") s
+        else if cut_exists "%================== Proof: ======================" s then
+          (kill_lines 0
+           o snd o cut_after "%================== Proof: ======================"
+           o fst o cut_before "==============  End of proof. ==================") s
+        else
+          raise SPASSError "Couldn't find a proof."
 
-fun extract_proof s
+(*fun extract_proof s
       = if cut_exists "Here is a proof with" s then
           (kill_lines 0
            o snd o cut_after ":"
@@ -144,7 +156,7 @@
            o fst o cut_after " ||  -> .") s
         else
           raise SPASSError "Couldn't find a proof."
-
+*)
 
 
 fun several p = many (some p)

--- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 16:12:49 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 16:18:49 2005 +0200
@@ -28,8 +28,9 @@
 
 datatype Side = Left |Right
 
- datatype Proofstep = ExtraAxiom
-                     |OrigAxiom
+ datatype Proofstep =  ExtraAxiom
+                     | OrigAxiom
+  		     | VampInput 
                      | Axiom
                      | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
                      | MRR of (int * int) * (int * int)