# HG changeset patch
# User mengj
# Date 1138008878 -3600
# Node ID 1d7b0830a8a7847a26cc4e0504783afda662506c
# Parent  7dd9aa160b6c583d6ffe28f492054943ec41613c
Fixed a bug.

diff -r 7dd9aa160b6c -r 1d7b0830a8a7 src/HOL/Tools/res_atp_setup.ML
--- a/src/HOL/Tools/res_atp_setup.ML	Sun Jan 22 22:16:34 2006 +0100
+++ b/src/HOL/Tools/res_atp_setup.ML	Mon Jan 23 10:34:38 2006 +0100
@@ -16,7 +16,7 @@
 val hol_partial_types = ResHolClause.partial_types;
 val hol_const_types_only = ResHolClause.const_types_only;
 val hol_no_types = ResHolClause.no_types;
-val hol_typ_level = ResHolClause.find_typ_level;
+fun hol_typ_level () = ResHolClause.find_typ_level ();
 
 fun is_typed_hol () = 
     let val tp_level = hol_typ_level()
@@ -84,22 +84,22 @@
 
 
 fun HOL_helper1 () =
-    let val tp_level = hol_typ_level ()
+    let val tp_level = !ResHolClause.typ_level
     in
-	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 ())
+	case tp_level of ResHolClause.T_PARTIAL => (warning "Partial type helper"; partial_typed_HOL_helper1 ())
+		       | ResHolClause.T_FULL => (warning "Full type helper"; full_typed_HOL_helper1 ())
+		       | ResHolClause.T_CONST => (warning "Const type helper"; const_typed_HOL_helper1 ())
+		       | ResHolClause.T_NONE => (warning "Untyped helper"; untyped_HOL_helper1 ())
     end;
 
 
 fun HOL_comb () =
-    let val tp_level = hol_typ_level ()
+    let val tp_level = !ResHolClause.typ_level
     in
-	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 ())
+	case tp_level of ResHolClause.T_FULL => (warning "Full type comb"; full_typed_comb ())
+		       | ResHolClause.T_PARTIAL => (warning "Partial type comb"; partial_typed_comb ())
+		       | ResHolClause.T_CONST => (warning "Const type comb"; const_typed_comb ())
+		       | ResHolClause.T_NONE => (warning "Untyped comb"; untyped_comb ())
     end;