1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 18:47:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Tue May 03 21:46:05 2011 +0200
     1.3 @@ -134,8 +134,8 @@
     1.4    | level_of_type_sys (Preds (_, level)) = level
     1.5    | level_of_type_sys (Tags (_, level)) = level
     1.6  
     1.7 -val is_type_level_virtually_sound =
     1.8 -  member (op =) [All_Types, Nonmonotonic_Types]
     1.9 +fun is_type_level_virtually_sound s =
    1.10 +  s = All_Types orelse s = Nonmonotonic_Types
    1.11  val is_type_sys_virtually_sound =
    1.12    is_type_level_virtually_sound o level_of_type_sys
    1.13