# HG changeset patch
# User mengj
# Date 1137729239 -3600
# Node ID caf9bc780c8086d91fd8fa58861f3ead627641d6
# Parent  02b310b1fa1038b76a721e727182567369e570fa
type information is now also printed.

diff -r 02b310b1fa10 -r caf9bc780c80 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Fri Jan 20 04:50:01 2006 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Fri Jan 20 04:53:59 2006 +0100
@@ -86,20 +86,20 @@
 fun HOL_helper1 () =
     let val tp_level = hol_typ_level ()
     in
-	case tp_level of T_FULL => full_typed_HOL_helper1 ()
-		       | T_PARTIAL => partial_typed_HOL_helper1 ()
-		       | T_CONST => const_typed_HOL_helper1 ()
-		       | T_NONE => untyped_HOL_helper1 ()
+	case tp_level of T_FULL => (warning "Full type"; full_typed_HOL_helper1 ())
+		       | T_PARTIAL => (warning "Partial type"; partial_typed_HOL_helper1 ())
+		       | T_CONST => (warning "Const type"; const_typed_HOL_helper1 ())
+		       | T_NONE => (warning "Untyped"; untyped_HOL_helper1 ())
     end;
 
 
 fun HOL_comb () =
     let val tp_level = hol_typ_level ()
     in
-	case tp_level of T_FULL => full_typed_comb ()
-		       | T_PARTIAL => partial_typed_comb ()
-		       | T_CONST => const_typed_comb ()
-		       | T_NONE => untyped_comb ()
+	case tp_level of T_FULL => (warning "Full type"; full_typed_comb ())
+		       | T_PARTIAL => (warning "Partial type"; partial_typed_comb ())
+		       | T_CONST => (warning "Const type"; const_typed_comb ())
+		       | T_NONE => (warning "Untyped"; untyped_comb ())
     end;