major simplification: removal of the goalstring argument
authorpaulson
Thu Oct 06 10:14:22 2005 +0200 (2005-10-06)
changeset 17772818cec5f82a4
parent 17771 1e07f6ab3118
child 17773 a7258e1020b7
major simplification: removal of the goalstring argument
src/HOL/Tools/ATP/AtpCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Oct 06 10:13:34 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/AtpCommunication.ML	Thu Oct 06 10:14:22 2005 +0200
     1.3 @@ -12,13 +12,13 @@
     1.4      val reconstruct : bool ref
     1.5      val checkEProofFound: 
     1.6            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
     1.7 -          string * string * (ResClause.clause * thm) Array.array -> bool
     1.8 +          string * (ResClause.clause * thm) Array.array -> bool
     1.9      val checkVampProofFound: 
    1.10            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.11 -          string * string * (ResClause.clause * thm) Array.array -> bool
    1.12 +          string * (ResClause.clause * thm) Array.array -> bool
    1.13      val checkSpassProofFound:  
    1.14            TextIO.instream * TextIO.outstream * Posix.Process.pid * 
    1.15 -          string * string * thm * int * (ResClause.clause * thm) Array.array -> bool
    1.16 +          string * thm * int * (ResClause.clause * thm) Array.array -> bool
    1.17    end;
    1.18  
    1.19  structure AtpCommunication : ATP_COMMUNICATION =
    1.20 @@ -64,7 +64,7 @@
    1.21  (*  and if so, transfer output to the input pipe of the main Isabelle process    *)
    1.22  (*********************************************************************************)
    1.23  
    1.24 -fun startTransfer (endS, fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.25 +fun startTransfer (endS, fromChild, toParent, ppid, probfile, clause_arr) =
    1.26   let fun transferInput currentString =
    1.27        let val thisLine = TextIO.inputLine fromChild
    1.28        in
    1.29 @@ -78,8 +78,8 @@
    1.30  			  	  then Recon_Transfer.vamp_lemma_list
    1.31  			  	  else Recon_Transfer.e_lemma_list
    1.32  	     in
    1.33 -	       trace ("\nExtracted_prf\n" ^ proofextract); 
    1.34 -	       lemma_list proofextract goalstring toParent ppid clause_arr
    1.35 +	       trace ("\nExtracted proof:\n" ^ proofextract); 
    1.36 +	       lemma_list proofextract probfile toParent ppid clause_arr
    1.37  	     end
    1.38  	else transferInput (currentString^thisLine)
    1.39        end
    1.40 @@ -87,34 +87,35 @@
    1.41       transferInput "";  true
    1.42   end handle EOF => false
    1.43  
    1.44 -fun signal_parent (toParent, ppid, msg, goalstring) =
    1.45 +
    1.46 +(*The signal handler in watcher.ML must be able to read the output of this.*)
    1.47 +fun signal_parent (toParent, ppid, msg, probfile) =
    1.48   (TextIO.output (toParent, msg);
    1.49 -  TextIO.output (toParent, goalstring);
    1.50 +  TextIO.output (toParent, probfile ^ "\n");
    1.51    TextIO.flushOut toParent;
    1.52 -  trace ("\nSignalled parent: " ^ msg);
    1.53 +  trace ("\nSignalled parent: " ^ msg ^ probfile);
    1.54    Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    1.55  
    1.56  (*Called from watcher. Returns true if the Vampire process has returned a verdict.*)
    1.57 -fun checkVampProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr) =
    1.58 +fun checkVampProofFound (fromChild, toParent, ppid, probfile, clause_arr) =
    1.59   let val thisLine = TextIO.inputLine fromChild
    1.60   in   
    1.61       trace thisLine;
    1.62       if thisLine = "" 
    1.63 -     then (trace "No proof output seen\n"; false)
    1.64 +     then (trace "\nNo proof output seen"; false)
    1.65       else if String.isPrefix start_V8 thisLine
    1.66 -     then
    1.67 -       startTransfer (end_V8, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.68 +     then startTransfer (end_V8, fromChild, toParent, ppid, probfile, clause_arr)
    1.69       else if (String.isPrefix "Satisfiability detected" thisLine) orelse
    1.70               (String.isPrefix "Refutation not found" thisLine)
    1.71 -     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
    1.72 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
    1.73  	   true)
    1.74       else
    1.75 -        checkVampProofFound  (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.76 +        checkVampProofFound  (fromChild, toParent, ppid, probfile, clause_arr)
    1.77    end
    1.78  
    1.79  
    1.80  (*Called from watcher. Returns true if the E process has returned a verdict.*)
    1.81 -fun checkEProofFound (fromChild, toParent, ppid,goalstring, childCmd, clause_arr) = 
    1.82 +fun checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr) = 
    1.83   let val thisLine = TextIO.inputLine fromChild  
    1.84   in   
    1.85       trace thisLine;
    1.86 @@ -122,15 +123,15 @@
    1.87       then (trace "No proof output seen\n"; false)
    1.88       else if String.isPrefix start_E thisLine
    1.89       then      
    1.90 -       startTransfer (end_E, fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
    1.91 +       startTransfer (end_E, fromChild, toParent, ppid, probfile, clause_arr)
    1.92       else if String.isPrefix "# Problem is satisfiable" thisLine
    1.93 -     then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
    1.94 +     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
    1.95  	   true)
    1.96       else if String.isPrefix "# Cannot determine problem status within resource limit" thisLine
    1.97 -     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
    1.98 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
    1.99  	   true)
   1.100       else
   1.101 -	checkEProofFound (fromChild, toParent, ppid, goalstring, childCmd, clause_arr)
   1.102 +	checkEProofFound (fromChild, toParent, ppid, probfile, clause_arr)
   1.103   end
   1.104  
   1.105  
   1.106 @@ -140,18 +141,19 @@
   1.107  (*  steps as a string to the input pipe of the main Isabelle process  *)
   1.108  (**********************************************************************)
   1.109  
   1.110 -fun spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
   1.111 -                    clause_arr = 
   1.112 +fun spass_reconstruct_tac proofextract toParent ppid probfile sg_num clause_arr = 
   1.113   SELECT_GOAL
   1.114    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
   1.115  	   METAHYPS(fn negs => 
   1.116 -  Recon_Transfer.spass_reconstruct proofextract goalstring toParent ppid negs clause_arr)]) sg_num;
   1.117 +		  Recon_Transfer.spass_reconstruct proofextract probfile 
   1.118 +				toParent ppid negs clause_arr)]) sg_num;
   1.119  
   1.120  
   1.121 -fun transferSpassInput (fromChild, toParent, ppid, goalstring, 
   1.122 +fun transferSpassInput (fromChild, toParent, ppid, probfile,
   1.123                          currentString, thm, sg_num, clause_arr) = 
   1.124   let val thisLine = TextIO.inputLine fromChild 
   1.125   in 
   1.126 +    trace thisLine;
   1.127      if thisLine = "" (*end of file?*)
   1.128      then (trace ("\nspass_extraction_failed: " ^ currentString);
   1.129  	  raise EOF)                    
   1.130 @@ -161,12 +163,12 @@
   1.131        in 
   1.132  	 trace ("\nextracted spass proof: " ^ proofextract);
   1.133  	 if !reconstruct 
   1.134 -	 then (spass_reconstruct_tac proofextract goalstring toParent ppid sg_num 
   1.135 +	 then (spass_reconstruct_tac proofextract toParent ppid probfile sg_num 
   1.136  		clause_arr thm; ())
   1.137 -	 else Recon_Transfer.spass_lemma_list proofextract goalstring 
   1.138 -	        toParent ppid clause_arr 
   1.139 +	 else Recon_Transfer.spass_lemma_list proofextract probfile toParent
   1.140 +	        ppid clause_arr 
   1.141        end
   1.142 -    else transferSpassInput (fromChild, toParent, ppid, goalstring,
   1.143 +    else transferSpassInput (fromChild, toParent, ppid, probfile,
   1.144  			     (currentString^thisLine), thm, sg_num, clause_arr)
   1.145   end;
   1.146  
   1.147 @@ -177,23 +179,22 @@
   1.148  (*********************************************************************************)
   1.149  
   1.150   
   1.151 -fun startSpassTransfer (fromChild, toParent, ppid, goalstring,childCmd,
   1.152 +fun startSpassTransfer (fromChild, toParent, ppid, probfile,
   1.153                          thm, sg_num,clause_arr) = 
   1.154     let val thisLine = TextIO.inputLine fromChild  
   1.155     in                 
   1.156        if thisLine = "" then false
   1.157        else if String.isPrefix "Here is a proof" thisLine then     
   1.158 -	 (trace ("\nabout to transfer proof, thm is " ^ string_of_thm thm);
   1.159 -	  transferSpassInput (fromChild, toParent, ppid, goalstring,thisLine, 
   1.160 +	 (trace ("\nabout to transfer SPASS proof\n:");
   1.161 +	  transferSpassInput (fromChild, toParent, ppid, probfile, thisLine, 
   1.162   	                     thm, sg_num,clause_arr);
   1.163  	  true) handle EOF => false
   1.164 -      else startSpassTransfer (fromChild, toParent, ppid, goalstring,
   1.165 -                               childCmd, thm, sg_num,clause_arr)
   1.166 +      else startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num,clause_arr)
   1.167      end
   1.168  
   1.169  
   1.170  (*Called from watcher. Returns true if the SPASS process has returned a verdict.*)
   1.171 -fun checkSpassProofFound (fromChild, toParent, ppid, goalstring, childCmd,
   1.172 +fun checkSpassProofFound (fromChild, toParent, ppid, probfile,
   1.173                            thm, sg_num, clause_arr) = 
   1.174   let val thisLine = TextIO.inputLine fromChild  
   1.175   in    
   1.176 @@ -201,17 +202,15 @@
   1.177       if thisLine = "" then (trace "No proof output seen\n"; false)
   1.178       else if thisLine = "SPASS beiseite: Proof found.\n"
   1.179       then      
   1.180 -        startSpassTransfer (fromChild, toParent, ppid, goalstring,
   1.181 -	                    childCmd, thm, sg_num, clause_arr)
   1.182 +        startSpassTransfer (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   1.183       else if thisLine = "SPASS beiseite: Completion found.\n"
   1.184 -     then (signal_parent (toParent, ppid, "Invalid\n", goalstring);
   1.185 +     then (signal_parent (toParent, ppid, "Invalid\n", probfile);
   1.186  	   true)
   1.187       else if thisLine = "SPASS beiseite: Ran out of time.\n" orelse
   1.188               thisLine = "SPASS beiseite: Maximal number of loops exceeded.\n"
   1.189 -     then (signal_parent (toParent, ppid, "Failure\n", goalstring);
   1.190 +     then (signal_parent (toParent, ppid, "Failure\n", probfile);
   1.191  	   true)
   1.192 -    else checkSpassProofFound (fromChild, toParent, ppid, goalstring,
   1.193 -                          childCmd, thm, sg_num, clause_arr)
   1.194 +    else checkSpassProofFound (fromChild, toParent, ppid, probfile, thm, sg_num, clause_arr)
   1.195   end
   1.196  
   1.197  end;
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 06 10:13:34 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 06 10:14:22 2005 +0200
     2.3 @@ -280,18 +280,19 @@
     2.4    | rules_to_string xs = "[" ^ space_implode ", " xs ^ "]"
     2.5  
     2.6  
     2.7 -fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
     2.8 +(*The signal handler in watcher.ML must be able to read the output of this.*)
     2.9 +fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
    2.10   let val _ = trace
    2.11                 ("\nGetting lemma names. proofstr is " ^ proofstr ^
    2.12 -                "\ngoalstring is " ^ goalstring ^
    2.13 -                "num of clauses is " ^ string_of_int (Array.length clause_arr))
    2.14 +                "\nprobfile is " ^ probfile ^
    2.15 +                "  num of clauses is " ^ string_of_int (Array.length clause_arr))
    2.16       val axiom_names = getax proofstr clause_arr
    2.17       val ax_str = rules_to_string axiom_names
    2.18      in 
    2.19  	 trace ("\nDone. Lemma list is " ^ ax_str);
    2.20           TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^
    2.21                    ax_str ^ "\n");
    2.22 -	 TextIO.output (toParent, goalstring);
    2.23 +	 TextIO.output (toParent, probfile ^ "\n");
    2.24  	 TextIO.flushOut toParent;
    2.25  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)
    2.26      end
    2.27 @@ -300,7 +301,7 @@
    2.28               Toplevel.exn_message exn);
    2.29        TextIO.output (toParent, "Translation failed for the proof: " ^ 
    2.30                       String.toString proofstr ^ "\n");
    2.31 -      TextIO.output (toParent, goalstring);
    2.32 +      TextIO.output (toParent, probfile);
    2.33        TextIO.flushOut toParent;
    2.34        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2));
    2.35  
    2.36 @@ -313,7 +314,7 @@
    2.37  
    2.38  (**** Full proof reconstruction for SPASS (not really working) ****)
    2.39  
    2.40 -fun spass_reconstruct proofstr goalstring toParent ppid thms clause_arr = 
    2.41 +fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = 
    2.42    let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
    2.43        val tokens = #1(lex proofstr)
    2.44  
    2.45 @@ -362,16 +363,16 @@
    2.46        val _ = trace ("\nReconstruction:\n" ^ reconstr)
    2.47    in 
    2.48         TextIO.output (toParent, reconstr^"\n");
    2.49 -       TextIO.output (toParent, goalstring);
    2.50 +       TextIO.output (toParent, probfile ^ "\n");
    2.51         TextIO.flushOut toParent;
    2.52         Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    2.53         all_tac
    2.54    end
    2.55    handle exn => (*FIXME: exn handler is too general!*)
    2.56     (trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn);
    2.57 -    TextIO.output (toParent,"Translation failed for the proof:"^
    2.58 +    TextIO.output (toParent,"Translation failed for SPASS proof:"^
    2.59           String.toString proofstr ^"\n");
    2.60 -    TextIO.output (toParent, goalstring);
    2.61 +    TextIO.output (toParent, probfile ^ "\n");
    2.62      TextIO.flushOut toParent;
    2.63      Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac)
    2.64  
    2.65 @@ -484,19 +485,6 @@
    2.66                          >>(fn (_,(a,_)) => a)
    2.67                       
    2.68  
    2.69 -
    2.70 -
    2.71 -fun anytoken_step input  = (word>> (fn (a) => a)  ) input
    2.72 -                       handle NOPARSE_WORD => (number>> (fn (a) => string_of_int a)  ) input
    2.73 -                      handle NOPARSE_NUMBER => (other_char >> (fn(a) => a)) input
    2.74 -
    2.75 -
    2.76 -
    2.77 -fun goalstring_step input= (anytoken_step ++ many (anytoken_step )
    2.78 -                  >> (fn (a,b) =>  (a^" "^(implode b)))) input
    2.79 -
    2.80 -
    2.81 -
    2.82   val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step
    2.83                  >> (fn (a, (b, (c,d))) => (a,(b,c,d)))
    2.84      
    2.85 @@ -630,7 +618,7 @@
    2.86  fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step)
    2.87  
    2.88  
    2.89 -fun to_isar_proof (frees, xs, goalstring) =
    2.90 +fun to_isar_proof (frees, xs) =
    2.91      let val extraaxioms = get_extraaxioms xs
    2.92  	val extraax_num = length extraaxioms
    2.93  	val origaxioms_and_steps = Library.drop (extraax_num, xs)  
    2.94 @@ -643,10 +631,9 @@
    2.95  	val steps = Library.drop (origax_num, axioms_and_steps)
    2.96  	val firststeps = ReconOrderClauses.butlast steps
    2.97  	val laststep = List.last steps
    2.98 -	val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
    2.99  	
   2.100  	val isar_proof = 
   2.101 -		("show \""^goalstring^"\"\n")^
   2.102 +		("show \"[your goal]\"\n")^
   2.103  		("proof (rule ccontr,skolemize, make_clauses) \n")^
   2.104  		("fix "^(frees_to_isar_str frees)^"\n")^
   2.105  		(assume_isar_extraaxioms extraaxioms)^
   2.106 @@ -670,13 +657,12 @@
   2.107  (* be passed over to the watcher, e.g.  numcls25       *)
   2.108  (*******************************************************)
   2.109  
   2.110 -fun apply_res_thm str goalstring  = 
   2.111 +fun apply_res_thm str  = 
   2.112    let val tokens = #1 (lex str);
   2.113 -      val _ = trace ("\napply_res_thm. str is: "^str^
   2.114 -                     "\ngoalstring is: \n"^goalstring^"\n")	
   2.115 +      val _ = trace ("\napply_res_thm. str is: "^str^"\n")	
   2.116        val (frees,recon_steps) = parse_step tokens 
   2.117    in 
   2.118 -      to_isar_proof (frees, recon_steps, goalstring)
   2.119 +      to_isar_proof (frees, recon_steps)
   2.120    end 
   2.121  
   2.122  end;
     3.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Oct 06 10:13:34 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Oct 06 10:14:22 2005 +0200
     3.3 @@ -17,8 +17,7 @@
     3.4  (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
     3.5  
     3.6  val callResProvers :
     3.7 -    TextIO.outstream * (string*string*string*string*string) list 
     3.8 -    -> unit
     3.9 +    TextIO.outstream * (string*string*string*string) list -> unit
    3.10  
    3.11  (* Send message to watcher to kill resolution provers *)
    3.12  val callSlayer : TextIO.outstream -> unit
    3.13 @@ -50,31 +49,18 @@
    3.14                else ();
    3.15  
    3.16  (*  The result of calling createWatcher  *)
    3.17 -datatype proc = PROC of {
    3.18 -        pid : Posix.Process.pid,
    3.19 -        instr : TextIO.instream,
    3.20 -        outstr : TextIO.outstream
    3.21 -      };
    3.22 +datatype proc = PROC of {pid : Posix.Process.pid,
    3.23 +			 instr : TextIO.instream,
    3.24 +			 outstr : TextIO.outstream};
    3.25  
    3.26  (*  The result of calling executeToList  *)
    3.27  datatype cmdproc = CMDPROC of {
    3.28          prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    3.29          cmd:  string,         (* The file containing the goal for res prover to prove *)     
    3.30 -        goalstring: string,   (* string representation of subgoal*) 
    3.31          proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    3.32          instr : TextIO.instream,   (*  Input stream to child process *)
    3.33          outstr : TextIO.outstream};  (*  Output stream from child process *)
    3.34  
    3.35 -type signal = Posix.Signal.signal
    3.36 -datatype exit_status = datatype Posix.Process.exit_status
    3.37 -
    3.38 -val fromStatus = Posix.Process.fromStatus
    3.39 -
    3.40 -fun reap(pid, instr, outstr) =
    3.41 -  let val u = TextIO.closeIn instr;
    3.42 -      val u = TextIO.closeOut outstr;
    3.43 -      val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    3.44 -  in status end
    3.45  
    3.46  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    3.47  	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    3.48 @@ -103,17 +89,13 @@
    3.49  
    3.50  fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
    3.51  
    3.52 -fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
    3.53 +fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = 
    3.54    (prover,(cmd, (instr,outstr)));
    3.55  
    3.56 -fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
    3.57 +fun cmdchildHandle (CMDPROC{prover,cmd,proc_handle,instr,outstr})  = 
    3.58    proc_handle;
    3.59  
    3.60 -fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    3.61 -  prover;
    3.62 -
    3.63 -fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
    3.64 -  goalstring;
    3.65 +fun cmdProver (CMDPROC{prover,cmd,proc_handle,instr,outstr}) = prover;
    3.66  
    3.67  
    3.68  (*    gets individual args from instream and concatenates them into a list      *)
    3.69 @@ -136,17 +118,13 @@
    3.70  fun callResProvers (toWatcherStr,  []) = 
    3.71        (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
    3.72  |   callResProvers (toWatcherStr,
    3.73 -                    (prover,goalstring, proverCmd,settings, 
    3.74 -                     probfile)  ::  args) =
    3.75 -      let val _ = trace (space_implode "\n" 
    3.76 -		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
    3.77 -			  probfile]))
    3.78 +                    (prover,proverCmd,settings,probfile)  ::  args) =
    3.79 +      let val _ = trace (space_implode ", " 
    3.80 +		         (["\ncallResProvers:", prover, proverCmd, probfile]))
    3.81        in TextIO.output (toWatcherStr,
    3.82                          (*Uses a special character to separate items sent to watcher*)
    3.83        	                space_implode (str command_sep)
    3.84 -                          [prover, proverCmd, settings, probfile,
    3.85 -                           String.toString goalstring ^ "\n"]);
    3.86 -              (*goalstring is a single string literal, with all specials escaped.*)
    3.87 +                          [prover, proverCmd, settings, probfile, "\n"]);
    3.88           goals_being_watched := (!goals_being_watched) + 1;
    3.89  	 TextIO.flushOut toWatcherStr;
    3.90  	 callResProvers (toWatcherStr,args)
    3.91 @@ -172,17 +150,16 @@
    3.92       else if thisLine = "Kill children\n"
    3.93       then (TextIO.output (toParentStr,thisLine); 
    3.94  	   TextIO.flushOut toParentStr;
    3.95 -	   [("","","Kill children",[],"")])
    3.96 +	   [("","Kill children",[],"")])
    3.97       else
    3.98 -       let val [prover,proverCmd,settingstr,probfile,goalstring] = 
    3.99 +       let val [prover,proverCmd,settingstr,probfile,_] = 
   3.100                     String.tokens (fn c => c = command_sep) thisLine
   3.101             val settings = String.tokens (fn c => c = setting_sep) settingstr
   3.102         in
   3.103 -           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
   3.104 -                  "  problem file: " ^ probfile ^ 
   3.105 -		  "\ngoalstring:  "^goalstring);
   3.106 +           trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd ^
   3.107 +                  "\n  problem file: " ^ probfile);
   3.108             getCmds (toParentStr, fromParentStr, 
   3.109 -                    (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
   3.110 +                    (prover, proverCmd, settings, probfile)::cmdList) 
   3.111         end
   3.112         handle Bind => 
   3.113            (trace "getCmds: command parsing failed!";
   3.114 @@ -215,8 +192,7 @@
   3.115  (* for tracing: encloses each string element in brackets. *)
   3.116  val concat_with_and = space_implode " & " o map (enclose "(" ")");
   3.117  
   3.118 -fun prems_string_of th =
   3.119 -  concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
   3.120 +fun prems_string_of th = concat_with_and (map string_of_cterm (cprems_of th))
   3.121  
   3.122  fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   3.123  
   3.124 @@ -239,13 +215,14 @@
   3.125  (*get the number of the subgoal from the filename: the last digit string*)
   3.126  fun number_from_filename s =
   3.127    case String.tokens (not o Char.isDigit) s of
   3.128 -      [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   3.129 +      [] => (trace ("\nWatcher could not read subgoal nunber! " ^ s); 
   3.130 +             raise ERROR)
   3.131      | numbers => valOf (Int.fromString (List.last numbers));
   3.132  
   3.133  fun setupWatcher (thm,clause_arr) = 
   3.134    let
   3.135 -    val p1 = Posix.IO.pipe ()   (** pipes for communication between parent and watcher **)
   3.136 -    val p2 = Posix.IO.pipe ()
   3.137 +    val p1 = Posix.IO.pipe()   (*pipes for communication between parent and watcher*)
   3.138 +    val p2 = Posix.IO.pipe()
   3.139      fun closep () = 
   3.140  	 (Posix.IO.close (#outfd p1); Posix.IO.close (#infd p1);
   3.141  	  Posix.IO.close (#outfd p2); Posix.IO.close (#infd p2))
   3.142 @@ -264,7 +241,7 @@
   3.143  	  val pid = Posix.ProcEnv.getpid()
   3.144  	  val () = Posix.ProcEnv.setpgid {pid = SOME pid, pgid = SOME pid}
   3.145                     (*set process group id: allows killing all children*)
   3.146 -	  val () = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   3.147 +	  val () = trace "\nsubgoals forked to startWatcher"
   3.148  	 
   3.149  	  fun pollChildInput fromStr = 
   3.150  	     case getInIoDesc fromStr of
   3.151 @@ -292,18 +269,16 @@
   3.152  		   val childIncoming = pollChildInput childInput
   3.153  		   val parentID = Posix.ProcEnv.getppid()
   3.154  		   val prover = cmdProver childProc
   3.155 -		   val prems_string = prems_string_of thm
   3.156 -		   val goalstring = cmdGoal childProc							
   3.157  	       in 
   3.158 -		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   3.159  		 if childIncoming
   3.160  		 then (* check here for prover label on child*)
   3.161  		   let val _ = trace ("\nInput available from child: " ^ childCmd ^ 
   3.162 -				      "\ngoalstring is " ^ goalstring)
   3.163 +				      "\nprover is " ^ prover)
   3.164  		       val childDone = (case prover of
   3.165 -			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   3.166 -			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   3.167 -			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   3.168 +			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)  
   3.169 +		         | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID, childCmd, clause_arr)             
   3.170 +			 | "spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID, childCmd, thm, sg_num,clause_arr)  
   3.171 +			 | _ => (trace "\nBad prover!"; true) )
   3.172  		    in
   3.173  		     if childDone
   3.174  		     then (* child has found a proof and transferred it *)
   3.175 @@ -323,117 +298,89 @@
   3.176  	(* settings should be a list of strings  ["-t 300", "-m 100000"]    *)
   3.177  	(* takes list of (string, string, string list, string)list proclist *)
   3.178  	fun execCmds [] procList = procList
   3.179 -	|   execCmds ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   3.180 -	      let val _ = trace (space_implode "\n" 
   3.181 -				 (["\nAbout to execute command for goal:",
   3.182 -				   goalstring, proverCmd] @ settings @
   3.183 -				  [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   3.184 +	|   execCmds ((prover,proverCmd,settings,file)::cmds) procList  =
   3.185 +	      let val _ = trace ("\nAbout to execute command: " ^ proverCmd ^ " " ^ 
   3.186 +	                         file)
   3.187  	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   3.188  		       Unix.execute(proverCmd, settings@[file])
   3.189  		  val (instr, outstr) = Unix.streamsOf childhandle
   3.190  		  val newProcList = CMDPROC{prover = prover,
   3.191  					    cmd = file,
   3.192 -					    goalstring = goalstring,
   3.193  					    proc_handle = childhandle,
   3.194  					    instr = instr,
   3.195  					    outstr = outstr} :: procList
   3.196 -     
   3.197 -		  val _ = trace ("\nFinished at " ^
   3.198 +     		  val _ = trace ("\nFinished at " ^
   3.199  			         Date.toString(Date.fromTimeLocal(Time.now())))
   3.200  	      in execCmds cmds newProcList end
   3.201  
   3.202           (******** Watcher Loop ********)
   3.203 -         val limit = ref 500;  (*don't let it run forever*)
   3.204 +         val limit = ref 200;  (*don't let it run forever*)
   3.205  
   3.206  	 fun keepWatching (procList) = 
   3.207  	   let fun loop procList =  
   3.208 -	      let val _ = trace ("\nCalling pollParentInput: " ^ Int.toString (!limit));
   3.209 +	      let val _ = trace ("\npollParentInput. Limit = " ^ Int.toString (!limit) ^ 
   3.210 +	                         "  length(procList) = " ^ Int.toString (length procList));
   3.211  		  val cmdsFromIsa = pollParentInput 
   3.212  				     (fromParentIOD, fromParentStr, toParentStr)
   3.213  	      in 
   3.214 -		 OS.Process.sleep (Time.fromMilliseconds 100);
   3.215 -		 limit := !limit - 1;
   3.216 -		 if !limit = 0 
   3.217 -		 then 
   3.218 -		  (trace "\nTimeout: Killing proof processes";
   3.219 -		   TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   3.220 -		   TextIO.flushOut toParentStr;
   3.221 -		   killChildren (map cmdchildHandle procList);
   3.222 -		   exit 0)
   3.223 -		 else case cmdsFromIsa of
   3.224 -		     SOME [(_,_,"Kill children",_,_)] => 
   3.225 -		       let val child_handles = map cmdchildHandle procList 
   3.226 -		       in  killChildren child_handles; loop []  end
   3.227 -		   | SOME cmds => (*  deal with commands from Isabelle process *)
   3.228 -		       if length procList < 40
   3.229 -		       then                        (* Execute locally  *)
   3.230 -			 let 
   3.231 -			   val newProcList = execCmds cmds procList
   3.232 -			   val newProcList' = checkChildren (newProcList, toParentStr) 
   3.233 -			 in
   3.234 -			   trace "\nJust execed a child"; loop newProcList'
   3.235 -			 end
   3.236 -		       else  (* Execute remotely [FIXME: NOT REALLY]  *)
   3.237 -			 let 
   3.238 -			   val newProcList = execCmds cmds procList
   3.239 -			   val newProcList' = checkChildren (newProcList, toParentStr) 
   3.240 -			 in loop newProcList' end
   3.241 -		   | NONE => (* No new input from Isabelle *)
   3.242 -		       let val newProcList = checkChildren (procList, toParentStr)
   3.243 -		       in
   3.244 -			 trace "\nNo new input, still watching"; loop newProcList
   3.245 -		       end
   3.246 +		OS.Process.sleep (Time.fromMilliseconds 100);
   3.247 +		limit := !limit - 1;
   3.248 +		if !limit = 0 
   3.249 +		then 
   3.250 +		 (trace "\nTimeout: Killing proof processes";
   3.251 +		  TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   3.252 +		  TextIO.flushOut toParentStr;
   3.253 +		  killChildren (map cmdchildHandle procList);
   3.254 +		  Posix.Process.exit 0w0)
   3.255 +		else case cmdsFromIsa of
   3.256 +		    SOME [(_,"Kill children",_,_)] => 
   3.257 +		      let val child_handles = map cmdchildHandle procList 
   3.258 +		      in  trace "\nReceived command to kill children";
   3.259 +			  killChildren child_handles; loop [] 
   3.260 +		      end
   3.261 +		  | SOME cmds => (*  deal with commands from Isabelle process *)
   3.262 +		      if length procList < 40
   3.263 +		      then                        (* Execute locally  *)
   3.264 +			let 
   3.265 +			  val _ = trace ("\nCommands from parent: " ^ Int.toString(length cmds))
   3.266 +			  val newProcList = execCmds cmds procList
   3.267 +			  val newProcList' = checkChildren (newProcList, toParentStr) 
   3.268 +			in
   3.269 +			  trace "\nCommands executed"; loop newProcList'
   3.270 +			end
   3.271 +		      else  (* Execute remotely [FIXME: NOT REALLY]  *)
   3.272 +			let 
   3.273 +			  val newProcList = execCmds cmds procList
   3.274 +			  val newProcList' = checkChildren (newProcList, toParentStr) 
   3.275 +			in loop newProcList' end
   3.276 +		  | NONE => (* No new input from Isabelle *)
   3.277 +		      let val newProcList = checkChildren (procList, toParentStr)
   3.278 +		      in
   3.279 +			trace "\nNothing from parent, still watching"; loop newProcList
   3.280 +		      end
   3.281  	       end
   3.282 -	   in  
   3.283 -	       loop procList
   3.284 -	   end
   3.285 -	   
   3.286 -
   3.287 +	   in  loop procList   end
   3.288  	 in
   3.289 -	  (*** Sort out pipes ********)
   3.290 -	   Posix.IO.close (#outfd p1);
   3.291 -	   Posix.IO.close (#infd p2);
   3.292 +	   (*** Sort out pipes ********)
   3.293 +	   Posix.IO.close (#outfd p1);  Posix.IO.close (#infd p2);
   3.294  	   Posix.IO.dup2{old = oldchildin, new = fromParent};
   3.295  	   Posix.IO.close oldchildin;
   3.296  	   Posix.IO.dup2{old = oldchildout, new = toParent};
   3.297  	   Posix.IO.close oldchildout;
   3.298 -
   3.299 -	   (* start the watcher loop  *)
   3.300 -	   keepWatching (procList);
   3.301 -	   (* fake return value - actually want the watcher to loop until killed *)
   3.302 -	   Posix.Process.wordToPid 0w0
   3.303 -	 end);
   3.304 -     (* end case *)
   3.305 -
   3.306 +	   keepWatching (procList)
   3.307 +	 end);   (* end case *)
   3.308  
   3.309      val _ = TextIO.flushOut TextIO.stdOut
   3.310 -
   3.311 -    (*******************************)
   3.312 -    (***  set watcher going ********)
   3.313 -    (*******************************)
   3.314 -
   3.315 -    val procList = []
   3.316 -    val pid = startWatcher procList
   3.317 -    (**************************************************)
   3.318 -    (* communication streams to watcher               *)
   3.319 -    (**************************************************)
   3.320 -
   3.321 +    val pid = startWatcher []
   3.322 +    (* communication streams to watcher*)
   3.323      val instr = openInFD ("_exec_in", #infd p2)
   3.324      val outstr = openOutFD ("_exec_out", #outfd p1)
   3.325 -    
   3.326    in
   3.327 -   (*******************************)
   3.328 -   (* close the child-side fds    *)
   3.329 -   (*******************************)
   3.330 -    Posix.IO.close (#outfd p2);
   3.331 -    Posix.IO.close (#infd p1);
   3.332 +   (* close the child-side fds*)
   3.333 +    Posix.IO.close (#outfd p2);  Posix.IO.close (#infd p1);
   3.334      (* set the fds close on exec *)
   3.335      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.336      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   3.337 -     
   3.338 -   (*******************************)
   3.339 -   (* return value                *)
   3.340 -   (*******************************)
   3.341      PROC{pid = pid, instr = instr, outstr = outstr}
   3.342    end;
   3.343  
   3.344 @@ -445,12 +392,17 @@
   3.345  
   3.346  fun killWatcher pid = Posix.Process.kill(Posix.Process.K_GROUP pid, Posix.Signal.kill);
   3.347  
   3.348 -fun reapWatcher(pid, instr, outstr) =
   3.349 +fun reapWatcher(pid, instr, outstr) = ignore
   3.350    (TextIO.closeIn instr; TextIO.closeOut outstr;
   3.351 -   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   3.352 +   Posix.Process.waitpid(Posix.Process.W_CHILD pid, []))
   3.353 +  handle OS.SysErr _ => ()
   3.354  
   3.355 -fun createWatcher (thm, clause_arr) =
   3.356 - let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   3.357 +fun string_of_subgoal th i =
   3.358 +    string_of_cterm (List.nth(cprems_of th, i-1))
   3.359 +    handle Subscript => "Subgoal number out of range!"
   3.360 +
   3.361 +fun createWatcher (th, clause_arr) =
   3.362 + let val (childpid,(childin,childout)) = childInfo (setupWatcher(th,clause_arr))
   3.363       fun decr_watched() =
   3.364  	  (goals_being_watched := !goals_being_watched - 1;
   3.365  	   if !goals_being_watched = 0
   3.366 @@ -459,30 +411,32 @@
   3.367  		     LargeWord.toString (Posix.Process.pidToWord childpid));
   3.368  	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   3.369  	    else ())
   3.370 -     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   3.371 +     val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of th);
   3.372       fun proofHandler n = 
   3.373         let val outcome = TextIO.inputLine childin
   3.374 -	   val goalstring = valOf (String.fromString (TextIO.inputLine childin))
   3.375 +	   val probfile = TextIO.inputLine childin
   3.376 +	   val sg_num = number_from_filename probfile
   3.377 +	   val text = string_of_subgoal th sg_num
   3.378  	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   3.379 -		        "\"\ngoalstring = " ^ goalstring ^
   3.380 +		        "\"\nprobfile = " ^ probfile ^
   3.381  		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   3.382         in 
   3.383  	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   3.384 -	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   3.385 +	 then (priority (Recon_Transfer.apply_res_thm outcome);
   3.386  	       decr_watched())
   3.387  	 else if String.isPrefix "Invalid" outcome
   3.388 -	 then (priority ("Subgoal is not provable:\n" ^ goalstring);
   3.389 +	 then (priority ("Subgoal is not provable:\n" ^ text);
   3.390  	       decr_watched())
   3.391  	 else if String.isPrefix "Failure" outcome
   3.392 -	 then (priority ("Proof attempt failed:\n" ^ goalstring);
   3.393 +	 then (priority ("Proof attempt failed:\n" ^ text);
   3.394  	       decr_watched()) 
   3.395  	(* print out a list of rules used from clasimpset*)
   3.396  	 else if String.isPrefix "Success" outcome
   3.397 -	 then (priority (outcome ^ goalstring);
   3.398 +	 then (priority (outcome ^ text);
   3.399  	       decr_watched())
   3.400  	  (* if proof translation failed *)
   3.401  	 else if String.isPrefix "Translation failed" outcome
   3.402 -	 then (priority (outcome ^ goalstring);
   3.403 +	 then (priority (outcome ^ text);
   3.404  	       decr_watched())
   3.405  	 else (priority "System error in proof handler";
   3.406  	       decr_watched())
     4.1 --- a/src/HOL/Tools/res_atp.ML	Thu Oct 06 10:13:34 2005 +0200
     4.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Oct 06 10:14:22 2005 +0200
     4.3 @@ -89,11 +89,9 @@
     4.4      fun make_atp_list [] n = []
     4.5        | make_atp_list (sg_term::xs) n =
     4.6            let
     4.7 -            val goalstring = Sign.string_of_term sign sg_term
     4.8              val probfile = prob_pathname n
     4.9              val time = Int.toString (!time_limit)
    4.10            in
    4.11 -            debug ("goalstring in make_atp_lists is\n" ^ goalstring);
    4.12              debug ("problem file in watcher_call_provers is " ^ probfile);
    4.13              (*Avoid command arguments containing spaces: Poly/ML and SML/NJ
    4.14                versions of Unix.execute treat them differently!*)
    4.15 @@ -111,7 +109,7 @@
    4.16                    val _ = ResLib.helper_path "SPASS_HOME" "SPASS"
    4.17                      (*We've checked that SPASS is there for ATP/spassshell to run.*)
    4.18                in 
    4.19 -                  ([("spass", goalstring,
    4.20 +                  ([("spass", 
    4.21                       getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",
    4.22                       optionline, probfile)] @ 
    4.23                    (make_atp_list xs (n+1)))
    4.24 @@ -120,14 +118,14 @@
    4.25  	    then 
    4.26                let val vampire = ResLib.helper_path "VAMPIRE_HOME" "vampire"
    4.27                in
    4.28 -                ([("vampire", goalstring, vampire, "-m 100000%-t " ^ time, probfile)] @
    4.29 +                ([("vampire", vampire, "-m 100000%-t " ^ time, probfile)] @
    4.30                   (make_atp_list xs (n+1)))       (*BEWARE! spaces in options!*)
    4.31                end
    4.32        	     else if !prover = "E"
    4.33        	     then
    4.34  	       let val Eprover = ResLib.helper_path "E_HOME" "eproof"
    4.35  	       in
    4.36 -		  ([("E", goalstring, Eprover, 
    4.37 +		  ([("E", Eprover, 
    4.38  		     "--tptp-in%-l5%-xAuto%-tAuto%--cpu-limit=" ^ time,
    4.39  		     probfile)] @
    4.40  		   (make_atp_list xs (n+1)))
    4.41 @@ -156,21 +154,20 @@
    4.42        val _ = debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    4.43        val write = if !prover = "spass" then dfg_inputs_tfrees else tptp_inputs_tfrees
    4.44        fun writenext n =
    4.45 -	if n=0 then ()
    4.46 +	if n=0 then []
    4.47  	 else
    4.48  	   (SELECT_GOAL
    4.49  	    (EVERY1 [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac, 
    4.50  	      METAHYPS(fn negs => 
    4.51  		(write (make_clauses negs) pf n 
    4.52  		       (axclauses,classrel_clauses,arity_clauses);
    4.53 -		 writenext (n-1); 
    4.54  		 all_tac))]) n th;
    4.55 -	    ())
    4.56 -      in writenext (length prems); clause_arr end;
    4.57 +	    pf n :: writenext (n-1))
    4.58 +      in (writenext (length prems), clause_arr) end;
    4.59  
    4.60  val last_watcher_pid =
    4.61 -  ref (NONE : (TextIO.instream * TextIO.outstream * Posix.Process.pid) option);
    4.62 -
    4.63 +  ref (NONE : (TextIO.instream * TextIO.outstream * 
    4.64 +               Posix.Process.pid * string list) option);
    4.65  
    4.66  (*writes out the current clasimpset to a tptp file;
    4.67    turns off xsymbol at start of function, restoring it at end    *)
    4.68 @@ -179,22 +176,24 @@
    4.69    if Thm.no_prems th then ()
    4.70    else
    4.71      let
    4.72 -      val _ = (*Set up signal handler to tidy away dead processes*)
    4.73 -	      IsaSignal.signal (IsaSignal.chld, 
    4.74 -	        IsaSignal.SIG_HANDLE (fn _ =>
    4.75 -		  (Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []);
    4.76 -		   debug "Child signal received\n")));  
    4.77 +      fun reap s = (*Signal handler to tidy away dead processes*)
    4.78 +	   (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
    4.79 +		SOME _ => reap s | NONE => ()) 
    4.80 +           handle OS.SysErr _ => ()
    4.81 +      val _ = 
    4.82 +	      IsaSignal.signal (IsaSignal.chld, IsaSignal.SIG_HANDLE reap)
    4.83        val _ = (case !last_watcher_pid of NONE => ()
    4.84 -               | SOME (_, childout, pid) => 
    4.85 +               | SOME (_, childout, pid, files) => 
    4.86                    (debug ("Killing old watcher, pid = " ^ 
    4.87                            Int.toString (ResLib.intOfPid pid));
    4.88 -                   Watcher.killWatcher pid))
    4.89 +                   Watcher.killWatcher pid;
    4.90 +                   ignore (map (try OS.FileSys.remove) files)))
    4.91                handle OS.SysErr _ => debug "Attempt to kill watcher failed";
    4.92 -      val clause_arr = write_problem_files prob_pathname (ctxt,th)
    4.93 +      val (files,clause_arr) = write_problem_files prob_pathname (ctxt,th)
    4.94        val (childin, childout, pid) = Watcher.createWatcher (th, clause_arr)
    4.95      in
    4.96 -      last_watcher_pid := SOME (childin, childout, pid);
    4.97 -      debug ("proof state: " ^ string_of_thm th);
    4.98 +      last_watcher_pid := SOME (childin, childout, pid, files);
    4.99 +      debug ("problem files: " ^ space_implode ", " files); 
   4.100        debug ("pid: " ^ Int.toString (ResLib.intOfPid pid));
   4.101        watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   4.102      end);
   4.103 @@ -217,8 +216,6 @@
   4.104          handle Proof.STATE _ => error "No goal present";
   4.105      val thy = ProofContext.theory_of ctxt;
   4.106    in
   4.107 -    debug ("initial thm in isar_atp:\n" ^ 
   4.108 -           Pretty.string_of (ProofContext.pretty_thm ctxt goal));
   4.109      debug ("subgoals in isar_atp:\n" ^ 
   4.110             Pretty.string_of (ProofContext.pretty_term ctxt
   4.111               (Logic.mk_conjunction_list (Thm.prems_of goal))));