# HG changeset patch # User blanchet # Date 1304544380 -7200 # Node ID 8a4682bf70edeb137d1a4805f66af41a868c9ae4 # Parent 7206f5688cade5fa183f647261e761ac1c3bc0d6 tuning diff -r 7206f5688cad -r 8a4682bf70ed src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- 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)