--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 11:03:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu May 12 15:29:18 2011 +0200
@@ -346,14 +346,12 @@
val atp_important_message_keep_quotient = 10
val fallback_best_type_systems =
- [Preds (Polymorphic, Const_Arg_Types), Simple All_Types]
+ [Preds (Polymorphic, Const_Arg_Types), Simple_Types All_Types]
-fun adjust_dumb_type_sys formats (Simple level) =
- if member (op =) formats Tff then (Tff, Simple level)
+fun adjust_dumb_type_sys formats (Simple_Types level) =
+ if member (op =) formats Tff then (Tff, Simple_Types level)
else (Fof, Preds (Mangled_Monomorphic, level))
- | adjust_dumb_type_sys formats type_sys =
- if member (op =) formats Fof then (Fof, type_sys)
- else (Tff, Simple (level_of_type_sys type_sys))
+ | adjust_dumb_type_sys formats type_sys = (hd formats, type_sys)
fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
adjust_dumb_type_sys formats type_sys
| determine_format_and_type_sys best_type_systems formats