src/HOL/Tools/ATP/recon_transfer_proof.ML

--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:02:14 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Sep 22 14:09:48 2005 +0200
@@ -301,9 +301,7 @@
 	 TextIO.output (toParent, "goalstring: "^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); ()
+	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
     end
     handle exn => (*FIXME: exn handler is too general!*)
      (File.write(File.tmp_path (Path.basic "proverString_handler")) 
@@ -312,9 +310,7 @@
                      remove_linebreaks proofstr ^ "\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); ());
+      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
 
 val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
 
@@ -383,10 +379,8 @@
        TextIO.output (toParent, reconstr^"\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
+       all_tac
   end
   handle exn => (*FIXME: exn handler is too general!*)
    (File.append(File.tmp_path (Path.basic "prover_reconstruction"))
@@ -395,9 +389,7 @@
          (remove_linebreaks proofstr) ^"\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)
+    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
 
 (**********************************************************************************)
 (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
@@ -699,10 +691,8 @@
       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)
+      to_isar_proof (frees, recon_steps, goalstring)
   end 
 
 end;