# 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