# HG changeset patch
# User paulson
# Date 1127990665 -7200
# Node ID 89932e53f31d6c6edf91e839bb362730e85d237c
# Parent  68583762ebdb507fd5a4daa0e115c7aece861ca9
moved concat_with_and to watcher.ML

diff -r 68583762ebdb -r 89932e53f31d src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 29 12:43:40 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 29 12:44:25 2005 +0200
@@ -220,8 +220,11 @@
 
 fun getProofCmd (a,c,d,e,f) = d
 
+(* for tracing: encloses each string element in brackets. *)
+val concat_with_and = space_implode " & " o map (enclose "(" ")");
+
 fun prems_string_of th =
-  Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
+  concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
 
 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
 
@@ -324,6 +327,7 @@
 		     then (* child has found a proof and transferred it *)
 			(* Remove this child and go on to check others*)
 			(Unix.reap child_handle;
+			 OS.FileSys.remove childCmd;
 			 checkChildren(otherChildren, toParentStr))
 		     else (* Keep this child and go on to check others  *)
 		       childProc :: checkChildren (otherChildren, toParentStr)
@@ -519,7 +523,7 @@
 	  (goals_being_watched := !goals_being_watched - 1;
 	   if !goals_being_watched = 0
 	   then 
-	     (trace ("\nReaping a watcher, childpid = "^
+	     (debug ("\nReaping a watcher, childpid = "^
 		     LargeWord.toString (Posix.Process.pidToWord childpid));
 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
 	    else ())
diff -r 68583762ebdb -r 89932e53f31d src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Sep 29 12:43:40 2005 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Sep 29 12:44:25 2005 +0200
@@ -84,10 +84,7 @@
 	| has (Abs(_,_,t)) = has t
 	| has _ = false
   in  has  end;
-
-(* for tracing: encloses each string element in brackets. *)
-val concat_with_and = space_implode " & " o map (enclose "(" ")");
-
+  
 
 (**** Clause handling ****)