src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 42682 562046fd8e0c
parent 42671 390de893659a
child 42684 2123b2608b14
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 04 19:47:41 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed May 04 22:47:13 2011 +0200
@@ -346,14 +346,14 @@
 val atp_important_message_keep_quotient = 10
 
 val fallback_best_type_systems =
-  [Preds (Polymorphic, Const_Arg_Types), Many_Typed]
+  [Preds (Polymorphic, Const_Arg_Types), Many_Typed All_Types]
 
-fun adjust_dumb_type_sys formats Many_Typed =
-    if member (op =) formats Tff then (Tff, Many_Typed)
-    else (Fof, Preds (Mangled_Monomorphic, All_Types))
+fun adjust_dumb_type_sys formats (Many_Typed level) =
+    if member (op =) formats Tff then (Tff, Many_Typed 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, Many_Typed)
+    else (Tff, Many_Typed (level_of_type_sys 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