# HG changeset patch
# User mengj
# Date 1154519301 -7200
# Node ID 16733b31e1cf7026daef7820307ae88c89732f04
# Parent  ad9fbbd01535c0062d2f298f0366acbbda8df45f
Only ignore too general axiom clauses, if the translation is partial- or constant-typed.

diff -r ad9fbbd01535 -r 16733b31e1cf src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Wed Aug 02 03:33:28 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Wed Aug 02 13:48:21 2006 +0200
@@ -174,6 +174,19 @@
 (* data types for typed combinator expressions        *)
 (******************************************************)
 
+datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
+
+val typ_level = ref T_CONST;
+
+fun full_types () = (typ_level:=T_FULL);
+fun partial_types () = (typ_level:=T_PARTIAL);
+fun const_types_only () = (typ_level:=T_CONST);
+fun no_types () = (typ_level:=T_NONE);
+
+
+fun find_typ_level () = !typ_level;
+
+
 type axiom_name = string;
 datatype kind = Axiom | Conjecture;
 fun name_of_kind Axiom = "axiom"
@@ -437,7 +450,7 @@
 	then error "Problem too trivial for resolution (empty clause)"
 	else if too_general lits then (Output.debug ("Omitting " ^ axiom_name ^ ": clause contains universal predicates"); raise MAKE_CLAUSE)
 	else
-	    if kind=Axiom andalso forall too_general_lit lits 
+	    if (!typ_level <> T_FULL) andalso kind=Axiom andalso forall too_general_lit lits 
 	    then (Output.debug ("Omitting " ^ axiom_name ^ ": equalities are too general"); raise MAKE_CLAUSE) 
 	else
 	    Clause {clause_id = clause_id, axiom_name = axiom_name, th = thm, kind = kind,
@@ -478,18 +491,6 @@
 
 val type_wrapper = "typeinfo";
 
-datatype type_level = T_FULL | T_PARTIAL | T_CONST | T_NONE;
-
-val typ_level = ref T_CONST;
-
-fun full_types () = (typ_level:=T_FULL);
-fun partial_types () = (typ_level:=T_PARTIAL);
-fun const_types_only () = (typ_level:=T_CONST);
-fun no_types () = (typ_level:=T_NONE);
-
-
-fun find_typ_level () = !typ_level;
-
 fun wrap_type (c,t) = 
     case !typ_level of T_FULL => type_wrapper ^ (ResClause.paren_pack [c,t])
 		     | _ => c;