# 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)