--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 23:21:11 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Wed May 04 23:26:20 2011 +0200
@@ -133,8 +133,8 @@
| level_of_type_sys (Preds (_, level)) = level
| level_of_type_sys (Tags (_, level)) = level
-fun is_type_level_virtually_sound s =
- s = All_Types orelse s = Nonmonotonic_Types
+fun is_type_level_virtually_sound level =
+ level = All_Types orelse level = Nonmonotonic_Types
val is_type_sys_virtually_sound =
is_type_level_virtually_sound o level_of_type_sys
@@ -142,6 +142,9 @@
is_type_level_virtually_sound level orelse level = Finite_Types
val is_type_sys_fairly_sound = is_type_level_fairly_sound o level_of_type_sys
+fun is_type_level_partial level =
+ level = Nonmonotonic_Types orelse level = Finite_Types
+
fun formula_map f (AQuant (q, xs, phi)) = AQuant (q, xs, formula_map f phi)
| formula_map f (AConn (c, phis)) = AConn (c, map (formula_map f) phis)
| formula_map f (AAtom tm) = AAtom (f tm)
@@ -1068,7 +1071,7 @@
(0 upto length helpers - 1 ~~ helpers)
|> (case type_sys of
Tags (Polymorphic, level) =>
- member (op =) [Finite_Types, Nonmonotonic_Types] level
+ is_type_level_partial level
? cons (ti_ti_helper_fact ())
| _ => I)),
(conjsN, map (formula_line_for_conjecture ctxt nonmono_Ts type_sys)