# HG changeset patch
# User paulson
# Date 1126193702 -7200
# Node ID 5bf0e0aacc24f7c9961f170a44e1f5be1ff59222
# Parent  04e21a27c0add7b0cf6b983da07680973b943131
consolidation of duplicate code in Isabelle-ATP linkup

diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Thu Sep 08 17:35:02 2005 +0200
@@ -22,7 +22,6 @@
 	 "Tools/ATP/recon_transfer_proof.ML"
 	 "Tools/ATP/VampCommunication.ML"
 	 "Tools/ATP/SpassCommunication.ML"
-     "Tools/ATP/ECommunication.ML"
 	 "Tools/ATP/watcher.ML"
 	 "Tools/ATP/res_clasimpset.ML"
 	 "Tools/res_atp.ML"
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/ECommunication.ML
--- a/src/HOL/Tools/ATP/ECommunication.ML	Thu Sep 08 16:09:23 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,222 +0,0 @@
-(*  Title:      SpassCommunication.ml
-    ID:         $Id$
-    Author:     Claire Quigley
-    Copyright   2004  University of Cambridge
-*)
-
-(***************************************************************************)
-(*  Code to deal with the transfer of proofs from a E process          *)
-(***************************************************************************)
-signature E_COMM =
-  sig
-    val E: bool ref
-    val getEInput : TextIO.instream -> string * string * string
-    val checkEProofFound: 
-          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
-          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
-  end;
-
-structure EComm : E_COMM =
-struct
-
-val E = ref false;
-
-exception EOF;
-
-(**********************************************************************)
-(*  Reconstruct the E proof w.r.t. thmstring (string version of   *)
-(*  Isabelle goal to be proved), then transfer the reconstruction     *)
-(*  steps as a string to the input pipe of the main Isabelle process  *)
-(**********************************************************************)
-
-fun reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
-                    clause_arr num_of_clauses = 
-   SELECT_GOAL
-    (EVERY1 [rtac ccontr, ResLib.atomize_tac, skolemize_tac, 
-             METAHYPS(fn negs => 
-    (Recon_Transfer.EString_to_lemmaString proofextract thmstring goalstring 
-              toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
-
-
-fun transferEInput (fromChild, toParent, ppid,thmstring,goalstring, 
-                    currentString, thm, sg_num,clause_arr, num_of_clauses) = 
- let val thisLine = TextIO.inputLine fromChild 
- in 
-     File.append (File.tmp_path (Path.basic "eprover_transfer"))
-		      ("transferEInput input line: " ^ thisLine);        
-    if thisLine = "" (*end of file?*)
-    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
-	  raise EOF)                    
-    else if thisLine = "# Proof object ends here.\n"
-    then 
-      let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
-      in 
-	  File.write (File.tmp_path (Path.basic"eprover_extracted_prf")) proofextract;
-	  reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num 
-	      clause_arr num_of_clauses thm
-      end
-    else transferEInput (fromChild, toParent, ppid,thmstring, goalstring,
-			     (currentString^thisLine), thm, sg_num, clause_arr, 
-			     num_of_clauses)
- end;
-
-
-(*********************************************************************************)
-(*  Inspect the output of an E process to see if it has found a proof,     *)
-(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
-(*********************************************************************************)
-
- 
-fun startETransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
-                    thm, sg_num,clause_arr, num_of_clauses) = 
-    let val thisLine = TextIO.inputLine fromChild  
-    in                 
-      if thisLine = "" then false
-      else if String.isPrefix "# Proof object starts" thisLine 
-      then     
-	 (File.append (File.tmp_path (Path.basic "eprover_transfer"))
-		      ("about to transfer proof, thm is: " ^ string_of_thm thm ^ "\n");
-	  transferEInput (fromChild, toParent, ppid,thmstring, goalstring,thisLine, 
-			      thm, sg_num,clause_arr, num_of_clauses);
-	  true) handle EOF => false
-      else startETransfer (fromChild, toParent, ppid, thmstring, goalstring,
-			       childCmd, thm, sg_num,clause_arr, num_of_clauses)
-     end
-
-
-fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
-                      thm, sg_num, clause_arr, num_of_clauses) = 
- let val E_proof_file = TextIO.openAppend
-	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
-     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
-			("checking if proof found, thm is: " ^ string_of_thm thm)
-     val thisLine = TextIO.inputLine fromChild  
- in   
-     if thisLine = "" 
-     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
-	    TextIO.closeOut E_proof_file;
-	    false)
-     else if (*thisLine = "# Problem is unsatisfiable (or provable), constructing proof object\n"*)
-	 thisLine = "# TSTP exit status: Unsatisfiable\n"
-     then      
-       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
-	startETransfer (fromChild, toParent, ppid, thmstring,goalstring,
-			childCmd, thm, sg_num, clause_arr, num_of_clauses))
-     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
-     then  
-       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
-	TextIO.output (toParent,childCmd^"\n" );
-	TextIO.flushOut toParent;
-	TextIO.output (E_proof_file, thisLine);
-	TextIO.closeOut E_proof_file;
-
-	TextIO.output (toParent, thisLine^"\n");
-	TextIO.output (toParent, thmstring^"\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
-	 true)
-     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
-     then  
-       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
-	TextIO.output (toParent, thisLine^"\n");
-	TextIO.output (toParent, thmstring^"\n");
-	TextIO.output (toParent, goalstring^"\n");
-	TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	TextIO.output (E_proof_file, "signalled parent\n");
-	TextIO.closeOut E_proof_file;
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1);
-	true)
-     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"                                                            		                 
-     then
-	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	 TextIO.output (toParent,childCmd^"\n" );
-	 TextIO.flushOut toParent;
-	 TextIO.output (toParent, thisLine);
-	 TextIO.flushOut toParent;
-	 true)
-     else
-	(TextIO.output (E_proof_file, thisLine);
-	TextIO.flushOut E_proof_file;
-	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
-	childCmd, thm, sg_num, clause_arr, num_of_clauses))
- end
-
-
-  
-(***********************************************************************)
-(*  Function used by the Isabelle process to read in an E proof   *)
-(***********************************************************************)
-
-fun getEInput instr = 
-    let val thisLine = TextIO.inputLine instr 
-        val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
-    in 
-      if thisLine = "" then ("No output from reconstruction process.\n","","")
-      else if String.sub (thisLine, 0) = #"["
-      then 
-	let val reconstr = thisLine
-	    val thmstring = TextIO.inputLine instr 
-	    val goalstring = TextIO.inputLine instr   
-	in
-	    (reconstr, thmstring, goalstring)
-	end
-      else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
-      then 
-	 let val reconstr = thisLine
-	     val thmstring = TextIO.inputLine instr
-	     val goalstring = TextIO.inputLine instr
-	 in
-	     (reconstr, thmstring, goalstring)
-	 end
-
-       else if String.isPrefix "# No proof" thisLine 
-      then 
-	 let val reconstr = thisLine
-	     val thmstring = TextIO.inputLine instr
-	     val goalstring = TextIO.inputLine instr
-	 in
-	     (reconstr, thmstring, goalstring)
-	 end
-
-       else if String.isPrefix "# Failure" thisLine 
-      then 
-	 let val reconstr = thisLine
-	     val thmstring = TextIO.inputLine instr
-	     val goalstring = TextIO.inputLine instr
-	 in
-	     (reconstr, thmstring, goalstring)
-	 end
-      else if String.isPrefix  "Rules from"  thisLine
-      then 
-	   let val reconstr = thisLine
-	       val thmstring = TextIO.inputLine instr
-	       val goalstring = TextIO.inputLine instr
-	   in
-	       (reconstr, thmstring, goalstring)
-	   end
-      else if substring (thisLine, 0,5) = "Proof"
-      then
-	let val reconstr = thisLine
-	    val thmstring = TextIO.inputLine instr
-	    val goalstring = TextIO.inputLine instr
-	in
-          File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
-          (reconstr, thmstring, goalstring)
-        end
-      else if substring (thisLine, 0,1) = "%"
-      then
-	let val reconstr = thisLine
-	    val thmstring = TextIO.inputLine instr
-	    val goalstring = TextIO.inputLine instr
-	in
-           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
-	   (reconstr, thmstring, goalstring)
-	end
-      else getEInput instr
-     end
-end;
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/SpassCommunication.ML
--- a/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Thu Sep 08 17:35:02 2005 +0200
@@ -48,7 +48,7 @@
  let val thisLine = TextIO.inputLine fromChild 
  in 
     if thisLine = "" (*end of file?*)
-    then (File.write (File.tmp_path (Path.basic"eprover_extraction_failed")) currentString;
+    then (File.write (File.tmp_path (Path.basic"spass_extraction_failed")) currentString;
 	  raise EOF)                    
     else if thisLine = "--------------------------SPASS-STOP------------------------------\n"
     then 
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/VampCommunication.ML
--- a/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Tools/ATP/VampCommunication.ML	Thu Sep 08 17:35:02 2005 +0200
@@ -9,6 +9,11 @@
 (***************************************************************************)
 signature VAMP_COMM =
   sig
+    val getEInput : TextIO.instream -> string * string * string
+    val checkEProofFound: 
+          TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
+          string * string * thm * int * (ResClause.clause * thm) Array.array * int -> bool
+
     val getVampInput : TextIO.instream -> string * string * string
     val checkVampProofFound: 
           TextIO.instream * TextIO.outstream * Posix.Process.pid * string *
@@ -21,7 +26,7 @@
 exception EOF;
 
 (**********************************************************************)
-(*  Reconstruct the Vampire proof w.r.t. thmstring (string version of   *)
+(*  Reconstruct the Vampire/E proof w.r.t. thmstring (string version of   *)
 (*  Isabelle goal to be proved), then transfer the reconstruction     *)
 (*  steps as a string to the input pipe of the main Isabelle process  *)
 (**********************************************************************)
@@ -32,121 +37,165 @@
       (EVERY1
         [rtac ccontr, ResLib.atomize_tac, skolemize_tac,
 	 METAHYPS(fn negs =>
-		     (Recon_Transfer.vampString_to_lemmaString proofextract thmstring 
+		     (Recon_Transfer.proverString_to_lemmaString proofextract thmstring 
 		       goalstring toParent ppid negs clause_arr num_of_clauses))]) sg_num
 
 
-fun transferVampInput (fromChild, toParent, ppid,thmstring,goalstring, 
-                       currentString, thm, sg_num,clause_arr, num_of_clauses) =
-  let val thisLine = TextIO.inputLine fromChild
-  in
-    if thisLine = "" (*end of file?*)
-    then (File.write (File.tmp_path (Path.basic"vampire_extraction_failed")) currentString;
-	  raise EOF)                    
-    else if (thisLine = "%==============  End of proof. ==================\n" )
-    then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
-	 in
-	   File.write (File.tmp_path (Path.basic"vampire_extracted_prf")) proofextract; 
-	   reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
-	                   clause_arr num_of_clauses thm
-	 end
-    else transferVampInput (fromChild, toParent, ppid,thmstring, goalstring, 
-             currentString^thisLine, thm, sg_num, clause_arr, num_of_clauses)
-  end;
-
-
 (*********************************************************************************)
-(*  Inspect the output of a Vampire process to see if it has found a proof,     *)
+(*  Inspect the output of an ATP process to see if it has found a proof,     *)
 (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
 (*********************************************************************************)
 
-
-fun startVampTransfer (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
-                       thm, sg_num,clause_arr, num_of_clauses) =
-    let val thisLine = TextIO.inputLine fromChild
-    in
-      if thisLine = "" then false
-      else if (thisLine = "%================== Proof: ======================\n")
-      then
-       (File.append (File.tmp_path (Path.basic "vampire_transfer"))
-		    ("about to transfer proof, thm is: " ^ string_of_thm thm);
-	transferVampInput (fromChild, toParent, ppid,thmstring, goalstring,
-			   thisLine, thm, sg_num,clause_arr, num_of_clauses);
-	true) handle EOF => false
-      else
-	 startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
-			    childCmd, thm, sg_num,clause_arr, num_of_clauses)
-    end
+fun startTransfer (startS,endS)
+      (fromChild, toParent, ppid, thmstring,goalstring,childCmd,
+       thm, sg_num,clause_arr, num_of_clauses) =
+ let val thisLine = TextIO.inputLine fromChild
+     fun transferInput currentString =
+      let val thisLine = TextIO.inputLine fromChild
+      in
+	if thisLine = "" (*end of file?*)
+	then (File.write (File.tmp_path (Path.basic"extraction_failed")) 
+	                 ("start bracket: " ^ startS ^
+	                  "\nend bracket: " ^ endS ^
+	                  "\naccumulated text: " ^ currentString);
+	      raise EOF)                    
+	else if String.isPrefix endS thisLine
+	then let val proofextract = Recon_Parse.extract_proof (currentString^thisLine)
+	     in
+	       File.write (File.tmp_path (Path.basic"extracted_prf")) proofextract; 
+	       reconstruct_tac proofextract thmstring goalstring toParent ppid sg_num  
+			       clause_arr num_of_clauses thm
+	     end
+	else transferInput (currentString^thisLine)
+      end
+ in
+   if thisLine = "" then false
+   else if String.isPrefix startS thisLine
+   then
+    (File.append (File.tmp_path (Path.basic "transfer_start"))
+		 ("about to transfer proof, thm is: " ^ string_of_thm thm);
+     transferInput thisLine;
+     true) handle EOF => false
+   else
+      startTransfer (startS,endS)
+                    (fromChild, toParent, ppid, thmstring, goalstring,
+		     childCmd, thm, sg_num,clause_arr, num_of_clauses)
+ end
 
 
 fun checkVampProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, 
                          thm, sg_num, clause_arr, num_of_clauses) =
- let val vamp_proof_file = TextIO.openAppend
-	   (File.platform_path(File.tmp_path (Path.basic "vampire_proof")))
-     val _ = File.write (File.tmp_path (Path.basic "vampire_checking_prf"))
+ let val proof_file = TextIO.openAppend
+	   (File.platform_path(File.tmp_path (Path.basic "atp_proof")))
+     val _ = File.write (File.tmp_path (Path.basic "atp_checking_prf"))
 			("checking if proof found, thm is: " ^ string_of_thm thm)
      val thisLine = TextIO.inputLine fromChild
  in   
      if thisLine = "" 
-     then (TextIO.output (vamp_proof_file, ("No proof output seen \n"));
-	   TextIO.closeOut vamp_proof_file;
+     then (TextIO.output (proof_file, "No proof output seen \n");
+	   TextIO.closeOut proof_file;
 	   false)
      else if thisLine = "% Proof found. Thanks to Tanya!\n"
      then
-      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
-       startVampTransfer (fromChild, toParent, ppid, thmstring, goalstring,
-			  childCmd, thm, sg_num, clause_arr, num_of_clauses))
-     else if (thisLine = "% Unprovable.\n" )
+       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
+	startTransfer (Recon_Parse.start_V6, Recon_Parse.end_V6)
+	      (fromChild, toParent, ppid, thmstring, goalstring,
+	       childCmd, thm, sg_num, clause_arr, num_of_clauses))
+     else if (thisLine = "% Unprovable.\n" ) orelse
+             (thisLine = "% Proof not found. Time limit expired.\n")
      then
-      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
-       TextIO.output (toParent,childCmd^"\n" );
-       TextIO.flushOut toParent;
-       TextIO.output (vamp_proof_file, thisLine);
-       TextIO.closeOut vamp_proof_file;
-       (*TextIO.output (toParent, thisLine);
+       (File.write (File.tmp_path (Path.basic "atp_response")) thisLine;
+	TextIO.output (toParent,childCmd^"\n");
 	TextIO.flushOut toParent;
-	TextIO.output (toParent, "bar\n");
-	TextIO.flushOut toParent;*)
-
-       TextIO.output (toParent, thisLine^"\n");
-       TextIO.output (toParent, thmstring^"\n");
-       TextIO.output (toParent, goalstring^"\n");
-       TextIO.flushOut toParent;
-       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-       (* Attempt to prevent several signals from turning up simultaneously *)
-       Posix.Process.sleep(Time.fromSeconds 1);
-       true)
-     else if (thisLine = "% Proof not found. Time limit expired.\n")
-     then
-      (File.write (File.tmp_path (Path.basic "vampire_response")) thisLine;
-       TextIO.output (toParent,childCmd^"\n" );
-       TextIO.flushOut toParent;
-       TextIO.output (vamp_proof_file, thisLine);
-       TextIO.closeOut vamp_proof_file;
-
-       TextIO.output (toParent, thisLine^"\n");
-       TextIO.output (toParent, thmstring^"\n");
-       TextIO.output (toParent, goalstring^"\n");
-       TextIO.flushOut toParent;
-       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-       (* Attempt to prevent several signals from turning up simultaneously *)
-       Posix.Process.sleep(Time.fromSeconds 1);
-       true)
+	TextIO.output (proof_file, thisLine);
+	TextIO.closeOut proof_file;
+ 
+	TextIO.output (toParent, thisLine^"\n");
+	TextIO.output (toParent, thmstring^"\n");
+	TextIO.output (toParent, goalstring^"\n");
+	TextIO.flushOut toParent;
+	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	(* Attempt to prevent several signals from turning up simultaneously *)
+	Posix.Process.sleep(Time.fromSeconds 1);
+	true)
      else
-       (TextIO.output (vamp_proof_file, thisLine);
-	TextIO.flushOut vamp_proof_file;
+       (TextIO.output (proof_file, thisLine);
+	TextIO.flushOut proof_file;
 	checkVampProofFound  (fromChild, toParent, ppid, thmstring,
 	   goalstring,childCmd, thm, sg_num, clause_arr, num_of_clauses))
   end
 
 
+fun checkEProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd,
+                      thm, sg_num, clause_arr, num_of_clauses) = 
+ let val E_proof_file = TextIO.openAppend
+	   (File.platform_path(File.tmp_path (Path.basic "eprover_proof")))
+     val _ = File.write (File.tmp_path (Path.basic "eprover_checking_prf"))
+			("checking if proof found, thm is: " ^ string_of_thm thm)
+     val thisLine = TextIO.inputLine fromChild  
+ in   
+     if thisLine = "" 
+     then (TextIO.output (E_proof_file, ("No proof output seen \n"));
+	    TextIO.closeOut E_proof_file;
+	    false)
+     else if thisLine = "# TSTP exit status: Unsatisfiable\n"
+     then      
+       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+       startTransfer (Recon_Parse.start_E, Recon_Parse.end_E)
+             (fromChild, toParent, ppid, thmstring, goalstring,
+	      childCmd, thm, sg_num, clause_arr, num_of_clauses))
+     else if thisLine= "# Problem is satisfiable (or invalid), generating saturation derivation\n"
+     then  
+       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+	TextIO.output (toParent,childCmd^"\n" );
+	TextIO.flushOut toParent;
+	TextIO.output (E_proof_file, thisLine);
+	TextIO.closeOut E_proof_file;
+
+	TextIO.output (toParent, thisLine^"\n");
+	TextIO.output (toParent, thmstring^"\n");
+	TextIO.output (toParent, goalstring^"\n");
+	TextIO.flushOut toParent;
+	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	(* Attempt to prevent several signals from turning up simultaneously *)
+	Posix.Process.sleep(Time.fromSeconds 1);
+	 true)
+     else if thisLine = "# Failure: Resource limit exceeded (time)\n" 
+     then  
+       (File.write (File.tmp_path (Path.basic "eprover_response")) thisLine;
+	TextIO.output (toParent, thisLine^"\n");
+	TextIO.output (toParent, thmstring^"\n");
+	TextIO.output (toParent, goalstring^"\n");
+	TextIO.flushOut toParent;
+	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	TextIO.output (E_proof_file, "signalled parent\n");
+	TextIO.closeOut E_proof_file;
+	(* Attempt to prevent several signals from turning up simultaneously *)
+	Posix.Process.sleep(Time.fromSeconds 1);
+	true)
+     else if thisLine = "# Failure: Resource limit exceeded (memory)\n"
+     then
+	(Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+	 TextIO.output (toParent,childCmd^"\n" );
+	 TextIO.flushOut toParent;
+	 TextIO.output (toParent, thisLine);
+	 TextIO.flushOut toParent;
+	 true)
+     else
+	(TextIO.output (E_proof_file, thisLine);
+	TextIO.flushOut E_proof_file;
+	checkEProofFound  (fromChild, toParent, ppid, thmstring,goalstring,
+	childCmd, thm, sg_num, clause_arr, num_of_clauses))
+ end
+
+
 (***********************************************************************)
 (*  Function used by the Isabelle process to read in a Vampire proof   *)
 (***********************************************************************)
 
 fun getVampInput instr =
     let val thisLine = TextIO.inputLine instr
-	val _ = File.write (File.tmp_path (Path.basic "vampire_line")) thisLine
+	val _ = File.write (File.tmp_path (Path.basic "atp_line")) thisLine
     in    (* reconstructed proof string *)
       if thisLine = "" then ("No output from reconstruction process.\n","","")
       else if String.sub (thisLine, 0) = #"[" orelse
@@ -166,4 +215,79 @@
       else getVampInput instr
     end
 
+
+(*FIXME!!: The following code is a mess. It mostly refers to SPASS-specific things*)
+
+(***********************************************************************)
+(*  Function used by the Isabelle process to read in an E proof   *)
+(***********************************************************************)
+
+fun getEInput instr = 
+    let val thisLine = TextIO.inputLine instr 
+        val _ = File.write (File.tmp_path (Path.basic "eprover_line")) thisLine
+    in 
+      if thisLine = "" then ("No output from reconstruction process.\n","","")
+      else if String.sub (thisLine, 0) = #"["
+      then 
+	let val reconstr = thisLine
+	    val thmstring = TextIO.inputLine instr 
+	    val goalstring = TextIO.inputLine instr   
+	in
+	    (reconstr, thmstring, goalstring)
+	end
+      else if String.isPrefix "SPASS beiseite:" thisLine (*FIXME: wrong!!*)
+      then 
+	 let val reconstr = thisLine
+	     val thmstring = TextIO.inputLine instr
+	     val goalstring = TextIO.inputLine instr
+	 in
+	     (reconstr, thmstring, goalstring)
+	 end
+
+       else if String.isPrefix "# No proof" thisLine 
+      then 
+	 let val reconstr = thisLine
+	     val thmstring = TextIO.inputLine instr
+	     val goalstring = TextIO.inputLine instr
+	 in
+	     (reconstr, thmstring, goalstring)
+	 end
+
+       else if String.isPrefix "# Failure" thisLine 
+      then 
+	 let val reconstr = thisLine
+	     val thmstring = TextIO.inputLine instr
+	     val goalstring = TextIO.inputLine instr
+	 in
+	     (reconstr, thmstring, goalstring)
+	 end
+      else if String.isPrefix  "Rules from"  thisLine
+      then 
+	   let val reconstr = thisLine
+	       val thmstring = TextIO.inputLine instr
+	       val goalstring = TextIO.inputLine instr
+	   in
+	       (reconstr, thmstring, goalstring)
+	   end
+      else if substring (thisLine, 0,5) = "Proof"
+      then
+	let val reconstr = thisLine
+	    val thmstring = TextIO.inputLine instr
+	    val goalstring = TextIO.inputLine instr
+	in
+          File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
+          (reconstr, thmstring, goalstring)
+        end
+      else if substring (thisLine, 0,1) = "%"
+      then
+	let val reconstr = thisLine
+	    val thmstring = TextIO.inputLine instr
+	    val goalstring = TextIO.inputLine instr
+	in
+           File.write (File.tmp_path (Path.basic "foo_getSpass")) thisLine;
+	   (reconstr, thmstring, goalstring)
+	end
+      else getEInput instr
+     end
+
 end;
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Thu Sep 08 17:35:02 2005 +0200
@@ -3,7 +3,6 @@
     Copyright   2004  University of Cambridge
 *)
 
-(*use "Translate_Proof";*)
 (* Parsing functions *)
 
 (* Auxiliary functions *)
@@ -115,6 +114,12 @@
           raise (GandalfError "Couldn't find a proof.")
 *)
 
+val start_E = "# Proof object starts here."
+val end_E   = "# Proof object ends here."
+val start_V6 = "%================== Proof: ======================"
+val end_V6   = "%==============  End of proof. =================="
+
+
 (*Identifies the start/end lines of an ATP's output*)
 fun extract_proof s =
   if cut_exists "Here is a proof with" s then
@@ -122,14 +127,14 @@
      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    (*Vampire 5.0*)
-     o snd o cut_after "%================== Proof: ======================"
-     o fst o cut_before "==============  End of proof. ==================") s
-  else if cut_exists "# Proof object ends here." s then
+  else if cut_exists start_V6 s then
+    (kill_lines 0    (*Vampire 6.0*)
+     o snd o cut_after start_V6
+     o fst o cut_before end_V6) s
+  else if cut_exists end_E s then
     (kill_lines 0    (*eproof*)
-     o snd o cut_after "# Proof object starts here."
-     o fst o cut_before "# Proof object ends here.") s
+     o snd o cut_after start_E
+     o fst o cut_before end_E) s
   else "??extract_proof failed" (*Couldn't find a proof*)
 
 fun several p = many (some p)
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 08 17:35:02 2005 +0200
@@ -137,13 +137,7 @@
 fun thmstrings [] str = str
 |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
 
-fun is_clasimp_ax clasimp_num n = n <=clasimp_num 
-
-
-
-fun retrieve_axioms clause_arr  [] = []
-|   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
- 						     (retrieve_axioms clause_arr  xs)
+fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
 
 fun subone x = x - 1
 
@@ -160,7 +154,7 @@
 	val _ = TextIO.output(axnums,(numstr clasimp_nums))
 	val _ = TextIO.closeOut(axnums)*)
     in
-	retrieve_axioms clause_arr clasimp_nums
+	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
     end
 
 
@@ -187,9 +181,18 @@
       clasimp_names
    end
    
- fun get_axiom_names_spass proof_steps thms clause_arr num_of_clauses  =
-   get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
-                       thms clause_arr num_of_clauses;
+
+fun get_axiom_names_spass proofstr thms clause_arr num_of_clauses =
+  let (* parse spass proof into datatype *)
+      val tokens = #1(lex proofstr)
+      val proof_steps = parse tokens
+      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
+                         ("Did parsing on "^proofstr)
+      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
+  in
+    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
+                    thms clause_arr num_of_clauses
+  end;
     
  fun get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses  =
    get_axiom_names (get_linenums proofstr) thms clause_arr num_of_clauses;
@@ -207,49 +210,49 @@
 
 fun addvars c (a,b)  = (a,b,c)
 
- fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
-     let 
-	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
-	val axioms = (List.filter is_axiom) proof_steps
-	val step_nums = get_step_nums axioms []
+fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
+  let 
+     val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
+     val axioms = (List.filter is_axiom) proof_steps
+     val step_nums = get_step_nums axioms []
 
-	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
-	
-	val vars = map thm_vars clauses
-       
-	val distvars = distinct (fold append vars [])
-	val clause_terms = map prop_of clauses  
-	val clause_frees = List.concat (map term_frees clause_terms)
+     val clauses =(*(clasimp_cls)@*)( make_clauses thms)
+     
+     val vars = map thm_vars clauses
+    
+     val distvars = distinct (fold append vars [])
+     val clause_terms = map prop_of clauses  
+     val clause_frees = List.concat (map term_frees clause_terms)
 
-	val frees = map lit_string_with_nums clause_frees;
+     val frees = map lit_string_with_nums clause_frees;
 
-	val distfrees = distinct frees
+     val distfrees = distinct frees
 
-	val metas = map Meson.make_meta_clause clauses
-	val ax_strs = map #3 axioms
+     val metas = map Meson.make_meta_clause clauses
+     val ax_strs = map #3 axioms
 
-	(* literals of -all- axioms, not just those used by spass *)
-	val meta_strs = map ReconOrderClauses.get_meta_lits metas
-       
-	val metas_and_strs = ListPair.zip (metas,meta_strs)
-	val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
-	val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
+     (* literals of -all- axioms, not just those used by spass *)
+     val meta_strs = map ReconOrderClauses.get_meta_lits metas
+    
+     val metas_and_strs = ListPair.zip (metas,meta_strs)
+     val _ = File.write(File.tmp_path (Path.basic "foo_clauses")) (onestr ax_strs)
+     val _ = File.write(File.tmp_path (Path.basic "foo_metastrs")) (onestr meta_strs)
 
-	(* get list of axioms as thms with their variables *)
+     (* get list of axioms as thms with their variables *)
 
-	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
-	val ax_vars = map thm_vars ax_metas
-	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
+     val ax_metas = get_assoc_snds ax_strs metas_and_strs []
+     val ax_vars = map thm_vars ax_metas
+     val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
 
-	(* get list of extra axioms as thms with their variables *)
-	val extra_metas = add_if_not_inlist metas ax_metas []
-	val extra_vars = map thm_vars extra_metas
-	val extra_with_vars = if (not (extra_metas = []) ) 
-			      then ListPair.zip (extra_metas,extra_vars)
-			      else []
-     in
-	(distfrees,distvars, extra_with_vars,ax_with_vars, (ListPair.zip (step_nums,ax_metas)))
-     end;
+     (* get list of extra axioms as thms with their variables *)
+     val extra_metas = add_if_not_inlist metas ax_metas []
+     val extra_vars = map thm_vars extra_metas
+     val extra_with_vars = if (not (extra_metas = []) ) 
+			   then ListPair.zip (extra_metas,extra_vars)
+			   else []
+  in
+     (distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas))
+  end;
                                             
 
 (*********************************************************************)
@@ -257,122 +260,24 @@
 (* Get out reconstruction steps as a string to be sent to Isabelle   *)
 (*********************************************************************)
 
-
 fun rules_to_string [] = "NONE"
   | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
-                                  
-
-(*val  proofstr = "1242[0:Inp] ||  -> equal(const_List_Orev(tconst_fun(tconst_List_Olist(U),tconst_List_Olist(U)),const_List_Olist_ONil),const_List_Olist_ONil)**.\
-\1279[0:Inp] ||  -> equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(U),tconst_nat),const_List_Olist_ONil),const_0)**.\
-\1430[0:Inp] || equal(const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Orev(tconst_fun(tconst_List_Olist(typ__Ha),tconst_List_Olist(typ__Ha)),const_List_Olist_ONil)),const_Nat_Osize(tconst_fun(tconst_List_Olist(typ__Ha),tconst_nat),const_List_Olist_ONil))** -> .\
-\1453[0:Rew:1279.0,1430.0,1242.0,1430.0,1279.0,1430.0] || equal(const_0,const_0)* -> .\
-\1454[0:Obv:1453.0] ||  -> .";*)
 
 fun subst_for a b = String.translate (fn c => str (if c=a then b else c));
 
 val remove_linebreaks = subst_for #"\n" #"\t";
 val restore_linebreaks = subst_for #"\t" #"\n";
 
-fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
-  let val _ = File.append(File.tmp_path (Path.basic"thmstringfile"))
-                  ("thmstring is: "^thmstring^"\n proofstr is: "^proofstr^"\n goalstr is: "^goalstring^" \n  num of clauses is: "^(string_of_int num_of_clauses))
-
-     (***********************************)
-     (* parse spass proof into datatype *)
-     (***********************************)
-      val tokens = #1(lex proofstr)
-      val proof_steps = parse tokens
-      val _ = File.write (File.tmp_path (Path.basic "parsing_done")) 
-                         ("Did parsing on "^proofstr)
-      val _ = File.write(File.tmp_path (Path.basic "parsing_thmstring"))
-                        ("Parsing for thmstring: "^thmstring)
-      (************************************)
-      (* recreate original subgoal as thm *)
-      (************************************)
-    
-      (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
-      (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
-      (* subgoal this is, and turn it into meta_clauses *)
-      (* should prob add array and table here, so that we can get axioms*)
-      (* produced from the clasimpset rather than the problem *)
-
-      val axiom_names = get_axiom_names_spass proof_steps thms clause_arr num_of_clauses
-      val ax_str = "Rules from clasimpset used in proof found by SPASS: " ^ 
-                   rules_to_string axiom_names 
-      val _ = File.append(File.tmp_path (Path.basic "reconstrfile"))
-                         ("reconstring is: "^ax_str^"  "^goalstring)       
-  in 
-       TextIO.output (toParent, ax_str^"\n");
-       TextIO.output (toParent, "goalstring: "^goalstring^"\n");
-       TextIO.output (toParent, "thmstring: "^thmstring^"\n");
-       TextIO.flushOut toParent;
-
-       Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-      (* Attempt to prevent several signals from turning up simultaneously *)
-       Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
-  end
-  handle _ => 
-  let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
-  in 
-     TextIO.output (toParent,"Proof found but parsing failed for resolution proof: "^(remove_linebreaks proofstr)^"\n" );
-       TextIO.output (toParent, (remove_linebreaks thmstring)^"\n");
-       TextIO.output (toParent, ( (remove_linebreaks goalstring)^"\n"));
-       TextIO.flushOut toParent;
-      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-      (* Attempt to prevent several signals from turning up simultaneously *)
-      Posix.Process.sleep(Time.fromSeconds 1); all_tac
-  end
 
-
-fun vampString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
+fun proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms clause_arr num_of_clauses getax = 
  let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
-               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
-                "goalstr is: "^goalstring^" num of clauses is: "^
-                (string_of_int num_of_clauses))
-
-    (***********************************)
-    (* get vampire axiom names         *)
-    (***********************************)
-
-     val axiom_names = get_axiom_names_vamp_E proofstr thms clause_arr num_of_clauses
-     val ax_str = "Rules from clasimpset used in proof found by Vampire: " ^
-                  rules_to_string axiom_names
-    in 
-	 File.append(File.tmp_path (Path.basic "reconstrfile")) 
-	            ("reconstring is: "^ax_str^"  "^goalstring);
-         TextIO.output (toParent, ax_str^"\n");
-	 TextIO.output (toParent, "goalstring: "^goalstring^"\n");
-	 TextIO.output (toParent, "thmstring: "^thmstring^"\n");
-	 TextIO.flushOut toParent;
+               ("thmstring is " ^ thmstring ^ 
+                "\nproofstr is " ^ proofstr ^
+                "\ngoalstr is " ^ goalstring ^
+                "\nnum of clauses is " ^ string_of_int num_of_clauses)
 
-	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
-    end
-    handle _ => 
-    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
-    in 
-	TextIO.output (toParent,"Proof found by Vampire but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
-	 TextIO.output (toParent, thmstring^"\n");
-	 TextIO.output (toParent, goalstring^"\n");
-	 TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	Posix.Process.sleep(Time.fromSeconds 1); all_tac
-    end;
-
-
-fun EString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
- let val _ = File.append(File.tmp_path (Path.basic "thmstringfile"))
-               (" thmstring is: "^thmstring^"proofstr is: "^proofstr^
-                "goalstr is: "^goalstring^" num of clauses is: "^
-                (string_of_int num_of_clauses))
-
-    (***********************************)
-    (* get E axiom names         *)
-    (***********************************)
-
-     val axiom_names = get_axiom_names_vamp_E proofstr  thms clause_arr  num_of_clauses
-     val ax_str = "Rules from clasimpset used in proof found by E: " ^
+     val axiom_names = getax proofstr thms clause_arr num_of_clauses
+     val ax_str = "Rules from clasimpset used in automatic proof: " ^
                   rules_to_string axiom_names
     in 
 	 File.append(File.tmp_path (Path.basic "reconstrfile"))
@@ -386,18 +291,29 @@
 	(* Attempt to prevent several signals from turning up simultaneously *)
 	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
     end
-    handle _ => 
-    let val _ = File.write(File.tmp_path (Path.basic "foo_handler")) "In exception handler"
-    in 
-	TextIO.output (toParent,"Proof found by E but translation failed for resolution proof: "^(remove_linebreaks proofstr) );
-	 TextIO.output (toParent, thmstring^"\n");
-	 TextIO.output (toParent, goalstring^"\n");
-	 TextIO.flushOut toParent;
-	Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
-	(* Attempt to prevent several signals from turning up simultaneously *)
-	Posix.Process.sleep(Time.fromSeconds 1); all_tac
-    end;
+    handle _ => (*FIXME: exn handler is too general!*)
+     (File.write(File.tmp_path (Path.basic "proverString_handler")) "In exception handler";
+      TextIO.output (toParent, "Proof found but translation failed : " ^ 
+                     remove_linebreaks proofstr ^ "\n");
+      TextIO.output (toParent, remove_linebreaks thmstring ^ "\n");
+      TextIO.output (toParent, remove_linebreaks goalstring ^ "\n");
+      TextIO.flushOut toParent;
+      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+      (* Attempt to prevent several signals from turning up simultaneously *)
+      Posix.Process.sleep(Time.fromSeconds 1); all_tac);
 
+fun proverString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
+      clause_arr num_of_clauses  = 
+  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
+       clause_arr num_of_clauses get_axiom_names_vamp_E;
+
+fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms
+      clause_arr  num_of_clauses  = 
+  proverString_to_lemmaString_aux proofstr thmstring goalstring toParent ppid thms        
+       clause_arr num_of_clauses get_axiom_names_spass;
+
+
+(**** Full proof reconstruction for SPASS (not really working) ****)
 
 fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   let val _ = File.write(File.tmp_path (Path.basic "thmstringfile")) 
@@ -792,29 +708,15 @@
 (* be passed over to the watcher, e.g.  numcls25       *)
 (*******************************************************)
 
-(* val str = "[S%x%P%R%Q%]1ExtraAxiom()[~ Q U%~ R U%][U%]2ExtraAxiom()[~ Q U%~ P U%][U%]3ExtraAxiom()[Q U%R U%][U%]1OrigAxiom()[S x%][]2OrigAxiom()[P U%R U%][U%]6OrigAxiom()[~ S U%~ P U%][U%]7OrigAxiom()[~ S U%~ R U%][U%]1Axiom()[S x%][]2Axiom()[R U%P U%][U%]6Axiom()[~ P U%~ S U%][U%]7Axiom()[~ R U%~ S U%][U%]8Binary((6,1),(1,0))[~ P x%][]9Binary((7,1),(1,0))[~ R x%][]19Binary((9,0),(2,0))[P x%][]25Binary((8,0),(19,0))[][]";
-
-val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
-
-val reconstr = "[P%Q%x%xa%]1OrigAxiom()[~ P U%][U%]3OrigAxiom()[Q U%][U%]5OrigAxiom()[P (x U)%~ Q (xa U)%][U%]9Binary((7,0),(3,0))[][]7Binary((1,0),(5,0))[~ Q (xa U)%][U%]5Axiom()[P (x U)%~ Q (xa U)%][U%]3Axiom()[Q U%][U%]1Axiom()[~ P U%][U%](ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)";
-
-
-val reconstr = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]";
-
-val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
-*)
+fun apply_res_thm str goalstring  = 
+  let val tokens = #1 (lex str);
+      val _ = File.append (File.tmp_path (Path.basic "apply_res_1")) 
+	 ("str is: "^str^" goalstr is: "^goalstring^"\n")	
+      val (frees,recon_steps) = parse_step tokens 
+      val isar_str = to_isar_proof (frees, recon_steps, goalstring)
+      val foo = File.write (File.tmp_path (Path.basic "apply_res_2")) isar_str
+  in 
+     Pretty.writeln(Pretty.str isar_str)
+  end 
 
-fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
-				val _ = File.append (File.tmp_path (Path.basic "applyres")) 
-			           ("str is: "^str^" goalstr is: "^goalstring^"\n")	
-                                   val (frees,recon_steps) = parse_step tokens 
-                                   val isar_str = to_isar_proof (frees, recon_steps, goalstring)
-                                   val foo =   TextIO.openOut (File.platform_path(File.tmp_path (Path.basic "foobar")));
-                               in 
-                                  TextIO.output(foo,(isar_str));TextIO.closeOut foo;Pretty.writeln(Pretty.str  isar_str); () 
-                               end 
-
-
-(* val reconstr = reconstr^"[P%]51Axiom()[~P%]52Axiom[P%][]53MRR((52,0),(51,0))[][]";
-*)
 end;
diff -r 04e21a27c0ad -r 5bf0e0aacc24 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 16:09:23 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 08 17:35:02 2005 +0200
@@ -434,7 +434,7 @@
 			      prems_string^prover^thmstring^goalstring^childCmd) 
 		       val childDone = (case prover of
 			   "vampire" => VampComm.checkVampProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  
-			    | "E" => EComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
+			    | "E" => VampComm.checkEProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)             
 			  |"spass" => SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)  )
 		    in
 		     if childDone      (**********************************************)