# HG changeset patch
# User paulson
# Date 1184681173 -7200
# Node ID 3fe991a1f80502edd7a09d452408c52c574a8ed9
# Parent  09ee9527ffcef7fd07194ac11dfe862c97bcc0a0
Full sort information by default.
Race condition on successful proofs fixed.

diff -r 09ee9527ffce -r 3fe991a1f805 src/HOL/Tools/res_reconstruct.ML
--- a/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:05:54 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:06:13 2007 +0200
@@ -33,7 +33,7 @@
 (*Full proof reconstruction wanted*)
 val full = ref true;
 
-val recon_sorts = ref false;
+val recon_sorts = ref true;
 
 val modulus = ref 1;    (*keep every nth proof line*)
 
@@ -512,7 +512,9 @@
     TextIO.output (toParent, "Success.\n");
     TextIO.output (toParent, probfile ^ "\n");
     TextIO.flushOut toParent;
-    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
+    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
+    (*Give the parent time to respond before possibly sending another signal*)
+    OS.Process.sleep (Time.fromMilliseconds 600)
   end;
 
 fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =