# HG changeset patch # User blanchet # Date 1304451965 -7200 # Node ID 45c650e5d0c67c1c5e06d8c8f13b697d518ea408 # Parent 8d53e7945078bd911ddeab1167796becedcad41e cosmetics diff -r 8d53e7945078 -r 45c650e5d0c6 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 03 18:47:22 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue May 03 21:46:05 2011 +0200 @@ -134,8 +134,8 @@ | level_of_type_sys (Preds (_, level)) = level | level_of_type_sys (Tags (_, level)) = level -val is_type_level_virtually_sound = - member (op =) [All_Types, Nonmonotonic_Types] +fun is_type_level_virtually_sound s = + s = All_Types orelse s = Nonmonotonic_Types val is_type_sys_virtually_sound = is_type_level_virtually_sound o level_of_type_sys