src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 16039 dfe264950511
parent 15919 b30a35432f5a
child 16061 8a139c1557bf
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun May 22 19:26:18 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon May 23 00:18:51 2005 +0200
     1.3 @@ -453,6 +453,10 @@
     1.4                                                in 
     1.5                                                    TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
     1.6                                                    TextIO.flushOut toParent;
     1.7 +						TextIO.output (toParent, thmstring^"\n");
     1.8 +                                         	   TextIO.flushOut toParent;
     1.9 +                                         	   TextIO.output (toParent, goalstring^"\n");
    1.10 +                                         	   TextIO.flushOut toParent;
    1.11              					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.12                                           	  (* Attempt to prevent several signals from turning up simultaneously *)
    1.13                                           	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac