Full sort information by default.
authorpaulson
Tue Jul 17 16:06:13 2007 +0200 (2007-07-17)
changeset 238333fe991a1f805
parent 23832 09ee9527ffce
child 23834 ad6ad61332fa
Full sort information by default.
Race condition on successful proofs fixed.
src/HOL/Tools/res_reconstruct.ML
     1.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:05:54 2007 +0200
     1.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Tue Jul 17 16:06:13 2007 +0200
     1.3 @@ -33,7 +33,7 @@
     1.4  (*Full proof reconstruction wanted*)
     1.5  val full = ref true;
     1.6  
     1.7 -val recon_sorts = ref false;
     1.8 +val recon_sorts = ref true;
     1.9  
    1.10  val modulus = ref 1;    (*keep every nth proof line*)
    1.11  
    1.12 @@ -512,7 +512,9 @@
    1.13      TextIO.output (toParent, "Success.\n");
    1.14      TextIO.output (toParent, probfile ^ "\n");
    1.15      TextIO.flushOut toParent;
    1.16 -    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    1.17 +    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.18 +    (*Give the parent time to respond before possibly sending another signal*)
    1.19 +    OS.Process.sleep (Time.fromMilliseconds 600)
    1.20    end;
    1.21  
    1.22  fun tstp_extract proofextract probfile toParent ppid ctxt th sgno thm_names =