1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu Sep 29 12:43:40 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu Sep 29 12:44:25 2005 +0200
     1.3 @@ -220,8 +220,11 @@
     1.4  
     1.5  fun getProofCmd (a,c,d,e,f) = d
     1.6  
     1.7 +(* for tracing: encloses each string element in brackets. *)
     1.8 +val concat_with_and = space_implode " & " o map (enclose "(" ")");
     1.9 +
    1.10  fun prems_string_of th =
    1.11 -  Meson.concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
    1.12 +  concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
    1.13  
    1.14  fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
    1.15  
    1.16 @@ -324,6 +327,7 @@
    1.17  		     then (* child has found a proof and transferred it *)
    1.18  			(* Remove this child and go on to check others*)
    1.19  			(Unix.reap child_handle;
    1.20 +			 OS.FileSys.remove childCmd;
    1.21  			 checkChildren(otherChildren, toParentStr))
    1.22  		     else (* Keep this child and go on to check others  *)
    1.23  		       childProc :: checkChildren (otherChildren, toParentStr)
    1.24 @@ -519,7 +523,7 @@
    1.25  	  (goals_being_watched := !goals_being_watched - 1;
    1.26  	   if !goals_being_watched = 0
    1.27  	   then 
    1.28 -	     (trace ("\nReaping a watcher, childpid = "^
    1.29 +	     (debug ("\nReaping a watcher, childpid = "^
    1.30  		     LargeWord.toString (Posix.Process.pidToWord childpid));
    1.31  	      killWatcher childpid; reapWatcher (childpid,childin, childout))
    1.32  	    else ())

     2.1 --- a/src/HOL/Tools/meson.ML	Thu Sep 29 12:43:40 2005 +0200
     2.2 +++ b/src/HOL/Tools/meson.ML	Thu Sep 29 12:44:25 2005 +0200
     2.3 @@ -84,10 +84,7 @@
     2.4  	| has (Abs(_,_,t)) = has t
     2.5  	| has _ = false
     2.6    in  has  end;
     2.7 -
     2.8 -(* for tracing: encloses each string element in brackets. *)
     2.9 -val concat_with_and = space_implode " & " o map (enclose "(" ")");
    2.10 -
    2.11 +  
    2.12  
    2.13  (**** Clause handling ****)
    2.14