# HG changeset patch
# User paulson
# Date 1148917082 -7200
# Node ID df6fd56d63a95e19c64348150c81a246ff5bb902
# Parent  73aab222fecbd231399d1a16d4fe7659559e26a8
warnings to debug outputs; default translation to const-typed

diff -r 73aab222fecb -r df6fd56d63a9 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Mon May 29 16:18:31 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Mon May 29 17:38:02 2006 +0200
@@ -512,7 +512,7 @@
 
 datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
 
-val typ_level = ref T_FULL;
+val typ_level = ref T_CONST;
 
 fun full_types () = (typ_level:=T_FULL);
 fun partial_types () = (typ_level:=T_PARTIAL);
@@ -830,17 +830,26 @@
 fun read_in fs = map (File.read o File.unpack_platform_path) fs; 
 
 fun get_helper_clauses_tptp () =
-    let val tlevel = case !typ_level of T_FULL => (warning "Fully-typed HOL"; "~~/src/HOL/Tools/atp-inputs/full_")
-				      | T_PARTIAL => (warning "Partially-typed HOL"; "~~/src/HOL/Tools/atp-inputs/par_")
-				      | T_CONST => (warning "Const-only-typed HOL"; "~~/src/HOL/Tools/atp-inputs/const_")
-				      | T_NONE => (warning "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_")
-	val helpers = if !include_combS then (warning "Include combinator S"; ["helper1.tptp","comb_inclS.tptp"]) else
-		     if !include_min_comb then (warning "Include min combinators"; ["helper1.tptp","comb_noS.tptp"])
-		     else (warning "No combinator is used"; ["helper1.tptp"])
-	val t_helpers = map (curry (op ^) tlevel) helpers
-    in
-	read_in t_helpers
-    end;
+  let val tlevel = case !typ_level of 
+		       T_FULL => (Output.debug "Fully-typed HOL"; 
+				  "~~/src/HOL/Tools/atp-inputs/full_")
+		     | T_PARTIAL => (Output.debug "Partially-typed HOL"; 
+				     "~~/src/HOL/Tools/atp-inputs/par_")
+		     | T_CONST => (Output.debug "Const-only-typed HOL"; 
+				   "~~/src/HOL/Tools/atp-inputs/const_")
+		     | T_NONE => (Output.debug "Untyped HOL"; 
+				  "~~/src/HOL/Tools/atp-inputs/u_")
+      val helpers = if !include_combS 
+                    then (Output.debug "Include combinator S"; 
+                          ["helper1.tptp","comb_inclS.tptp"]) 
+                    else if !include_min_comb 
+                    then (Output.debug "Include min combinators"; 
+                          ["helper1.tptp","comb_noS.tptp"])
+		    else (Output.debug "No combinator is used"; ["helper1.tptp"])
+      val t_helpers = map (curry (op ^) tlevel) helpers
+  in
+      read_in t_helpers
+  end;
 	
 						  
 (* write TPTP format to a single file *)
@@ -865,17 +874,26 @@
 
 (* dfg format *)
 fun get_helper_clauses_dfg () = 
-    let val tlevel = case !typ_level of T_FULL => (warning "Fully-typed HOL"; "~~/src/HOL/Tools/atp-inputs/full_")
-				      | T_PARTIAL => (warning "Partially-typed HOL"; "~~/src/HOL/Tools/atp-inputs/par_")
-				      | T_CONST => (warning "Const-only-typed HOL"; "~~/src/HOL/Tools/atp-inputs/const_")
-				      | T_NONE => (warning "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_")
-	val helpers = if !include_combS then (warning "Include combinator S"; ["helper1.dfg","comb_inclS.dfg"]) else
-		      if !include_min_comb then (warning "Include min combinators"; ["helper1.dfg","comb_noS.dfg"])
-		      else (warning "No combinator is used"; ["helper1.dfg"])
-	val t_helpers = map (curry (op ^) tlevel) helpers
-    in
-	read_in t_helpers
-    end;
+ let val tlevel = case !typ_level of 
+                      T_FULL => (Output.debug "Fully-typed HOL"; 
+                                 "~~/src/HOL/Tools/atp-inputs/full_")
+		    | T_PARTIAL => (Output.debug "Partially-typed HOL"; 
+		                    "~~/src/HOL/Tools/atp-inputs/par_")
+		    | T_CONST => (Output.debug "Const-only-typed HOL"; 
+		                  "~~/src/HOL/Tools/atp-inputs/const_")
+		    | T_NONE => (Output.debug "Untyped HOL"; 
+		                 "~~/src/HOL/Tools/atp-inputs/u_")
+     val helpers = if !include_combS 
+                   then (Output.debug "Include combinator S"; 
+                         ["helper1.dfg","comb_inclS.dfg"]) else
+		   if !include_min_comb 
+		   then (Output.debug "Include min combinators"; 
+		         ["helper1.dfg","comb_noS.dfg"])
+		   else (Output.debug "No combinator is used"; ["helper1.dfg"])
+     val t_helpers = map (curry (op ^) tlevel) helpers
+ in
+     read_in t_helpers
+ end;
 
 
 fun dfg_write_file  thms filename (axclauses,classrel_clauses,arity_clauses) =