# HG changeset patch
# User quigley
# Date 1119017929 -7200
# Node ID 5d0d24bd2c96f46a97391a8f31d49b41a8a7321e
# Parent  9bc16273c2d45c70d47dc408274b917bd4270e48
Multiple subgoals working.

diff -r 9bc16273c2d4 -r 5d0d24bd2c96 src/HOL/Tools/ATP/recon_parse.ML
--- 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)
diff -r 9bc16273c2d4 -r 5d0d24bd2c96 src/HOL/Tools/ATP/recon_translate_proof.ML
--- 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)