# HG changeset patch
# User paulson
# Date 1141990118 -3600
# Node ID 1f5b5dc3f48a529218be9ab788261cc409ba3121
# Parent  c8879dd3a95364f978bb3bf462df2404a6ea1e3e
Changed some warnings to debug messages

diff -r c8879dd3a953 -r 1f5b5dc3f48a src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Mar 10 12:27:36 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Fri Mar 10 12:28:38 2006 +0100
@@ -301,9 +301,9 @@
 	       (change clause_cache (Symtab.update (name, (th, cls))); (cls,thy')))
     | SOME (th',cls) =>
         if eq_thm(th,th') then (cls,thy)
-	else (warning ("skolem_cache: Ignoring variant of theorem " ^ name); 
-	      warning (string_of_thm th);
-	      warning (string_of_thm th');
+	else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name); 
+	      Output.debug (string_of_thm th);
+	      Output.debug (string_of_thm th');
 	      ([th],thy));
 	      
 fun skolem_cache ((name,th), thy) = #2 (skolem_cache_thm ((name,th), thy));
@@ -319,9 +319,9 @@
 		  in change clause_cache (Symtab.update (s, (th, cls))); cls end
 	      | SOME(th',cls) =>
 		  if eq_thm(th,th') then cls
-		  else (warning ("cnf_axiom: duplicate or variant of theorem " ^ name); 
-		        warning (string_of_thm th);
-		        warning (string_of_thm th');
+		  else (Output.debug ("cnf_axiom: duplicate or variant of theorem " ^ name); 
+		        Output.debug (string_of_thm th);
+		        Output.debug (string_of_thm th');
 		        cls);
 
 fun pairname th = (Thm.name_of_thm th, th);