# HG changeset patch
# User blanchet
# Date 1304267845 -7200
# Node ID 562d6415616a5631f829513ef4cb79ef5b2a8304
# Parent  4fbb1de05169c33ab8ce653a9e2393b29766a4c5
take "partial_types" option with a grain of salt

diff -r 4fbb1de05169 -r 562d6415616a src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:25 2011 +0200
@@ -345,7 +345,7 @@
   | type_sys_monomorphizes (Tags (mono, _)) = mono
   | type_sys_monomorphizes No_Types = false
 
-val fallback_best_type_systems = [Many_Typed, Args (false, Unsound)]
+val fallback_best_type_systems = [Args (false, Unsound), Many_Typed]
 
 fun adjust_dumb_type_sys formats Many_Typed =
     if member (op =) formats Tff then (Tff, Many_Typed)
@@ -358,7 +358,7 @@
   | determine_format_and_type_sys best_type_systems formats
                                   (Smart_Type_Sys full_types) =
     best_type_systems @ fallback_best_type_systems
-    |> filter (fn type_sys => (level_of_type_sys type_sys = Sound) = full_types)
+    |> full_types ? filter (curry (op =) Sound o level_of_type_sys)
     |> hd |> adjust_dumb_type_sys formats
 
 fun run_atp auto name