# HG changeset patch
# User paulson
# Date 1148917110 -7200
# Node ID 9ac97dc142148c4dbc6c312af5b0adf2f3193f03
# Parent  df6fd56d63a95e19c64348150c81a246ff5bb902
warnings to debug outputs

diff -r df6fd56d63a9 -r 9ac97dc14214 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Mon May 29 17:38:02 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon May 29 17:38:30 2006 +0200
@@ -207,7 +207,7 @@
 			  else fn_lg f (FOL,seen)
 	val _ =
           if is_fol_logic lg' then ()
-          else warning ("Found a HOL term: " ^ Display.raw_string_of_term f)
+          else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f)
 	 in
 	     term_lg (args@tms) (lg',seen')
     end
@@ -230,7 +230,7 @@
 			  else pred_lg pred (lg,seen)
 	val _ =
           if is_fol_logic lg' then ()
-          else warning ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
+          else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred)
     in
 	term_lg args (lg',seen')
     end;
@@ -240,7 +240,7 @@
     let val (lg,seen') = lit_lg lit (FOL,seen)
 	val _ =
           if is_fol_logic lg then ()
-          else warning ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
+          else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit)
     in
 	lits_lg lits (lg,seen')
     end
@@ -265,7 +265,7 @@
     let val (lg,seen') = logic_of_clause cls (FOL,seen)
 	val _ =
           if is_fol_logic lg then ()
-          else warning ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
+          else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
     in
 	logic_of_clauses clss (lg,seen')
     end
@@ -325,16 +325,16 @@
 	val file = atp_input_file()
     in
 	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
-	 warning ("Writing to " ^ file);
+	 Output.debug ("Writing to " ^ file);
 	 file)
     end;
 
 
 (**** remove tmp files ****)
 fun cond_rm_tmp file = 
-    if !keep_atp_input then warning "ATP input kept..." 
-    else if !destdir <> "" then warning ("ATP input kept in directory " ^ (!destdir))
-    else (warning "deleting ATP inputs..."; OS.FileSys.remove file);
+    if !keep_atp_input then Output.debug "ATP input kept..." 
+    else if !destdir <> "" then Output.debug ("ATP input kept in directory " ^ (!destdir))
+    else (Output.debug "deleting ATP inputs..."; OS.FileSys.remove file);
 
 
 (****** setup ATPs as Isabelle methods ******)