make sure the minimizer monomorphizes when it should

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Sun May 01 18:37:24 2011 +0200
@@ -14,9 +14,9 @@
 
   datatype type_system =
     Many_Typed |
-    Tags of bool |
+    Mangled of bool |
     Args of bool |
-    Mangled of bool |
+    Tags of bool |
     No_Types
 
   val fact_prefix : string
@@ -81,15 +81,15 @@
 
 datatype type_system =
   Many_Typed |
-  Tags of bool |
+  Mangled of bool |
   Args of bool |
-  Mangled of bool |
+  Tags of bool |
   No_Types
 
 fun is_type_system_sound Many_Typed = true
-  | is_type_system_sound (Tags full_types) = full_types
+  | is_type_system_sound (Mangled full_types) = full_types
   | is_type_system_sound (Args full_types) = full_types
-  | is_type_system_sound (Mangled full_types) = full_types
+  | is_type_system_sound (Tags full_types) = full_types
   | is_type_system_sound No_Types = false
 
 fun type_system_types_dangerous_types (Tags _) = true
@@ -100,12 +100,12 @@
   (member (op =) [@{const_name HOL.eq}] s orelse
    case type_sys of
      Many_Typed => false
-   | Tags full_types => full_types orelse s = explicit_app_base
+   | Mangled _ => false
    | Args _ => s = explicit_app_base
-   | Mangled _ => false
+   | Tags full_types => full_types orelse s = explicit_app_base
    | No_Types => true)
 
-datatype type_arg_policy = No_Type_Args | Explicit_Type_Args | Mangled_Types
+datatype type_arg_policy = No_Type_Args | Mangled_Types | Explicit_Type_Args
 
 fun type_arg_policy type_sys s =
   if dont_need_type_args type_sys s then
@@ -501,8 +501,8 @@
            let val s'' = invert_const s'' in
              case type_arg_policy type_sys s'' of
                No_Type_Args => (name, [])
+             | Mangled_Types => (mangled_const_name ty_args name, [])
              | Explicit_Type_Args => (name, ty_args)
-             | Mangled_Types => (mangled_const_name ty_args name, [])
            end)
         |> (fn (name, ty_args) => CombConst (name, ty, ty_args))
       | aux tm = tm
@@ -551,7 +551,7 @@
     val do_bound_type =
       if type_sys = Many_Typed then SOME o mangled_combtyp else K NONE
     val do_out_of_bound_type =
-      if member (op =) [Args true, Mangled true] type_sys then
+      if member (op =) [Mangled true, Args true] type_sys then
         (fn (s, ty) =>
             type_pred_combatom type_sys ty (CombVar (s, ty))
             |> formula_for_combformula ctxt type_sys |> SOME)
@@ -770,7 +770,7 @@
 
 (* FIXME: needed? *)
 fun const_table_for_facts type_sys sym_tab facts =
-  Symtab.empty |> member (op =) [Many_Typed, Args true, Mangled true] type_sys
+  Symtab.empty |> member (op =) [Many_Typed, Mangled true, Args true] type_sys
                   ? fold (consider_fact_consts type_sys sym_tab) facts
 
 fun strip_and_map_combtyp 0 f ty = ([], f ty)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun May 01 18:37:24 2011 +0200
@@ -235,21 +235,21 @@
     val blocking = auto orelse debug orelse lookup_bool "blocking"
     val provers = lookup_string "provers" |> space_explode " "
                   |> auto ? single o hd
-    val (type_sys, must_monomorphize) =
+    val type_sys =
       case (lookup_string "type_sys", lookup_bool "full_types") of
-        ("many_typed", _) => (Many_Typed, true)
-      | ("tags", full_types) => (Tags full_types, false)
-      | ("args", full_types) => (Args full_types, false)
-      | ("mangled", full_types) => (Mangled full_types, true)
-      | ("none", false) => (No_Types, false)
+        ("many_typed", _) => Many_Typed
+      | ("mangled", full_types) => Mangled full_types
+      | ("args", full_types) => Args full_types
+      | ("tags", full_types) => Tags full_types
+      | ("none", false) => No_Types
       | (type_sys, full_types) =>
         if member (op =) ["none", "smart"] type_sys then
-          (if full_types then Tags true else Args false, false)
+          if full_types then Tags true else Args false
         else
           error ("Unknown type system: " ^ quote type_sys ^ ".")
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_int_option "max_relevant"
-    val monomorphize = must_monomorphize orelse lookup_bool "monomorphize"
+    val monomorphize = lookup_bool "monomorphize"
     val monomorphize_limit = lookup_int "monomorphize_limit"
     val explicit_apply = lookup_bool "explicit_apply"
     val isar_proof = lookup_bool "isar_proof"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun May 01 18:37:24 2011 +0200
@@ -334,6 +334,10 @@
    them each time. *)
 val atp_important_message_keep_factor = 0.1
 
+fun must_monomorphize Many_Typed = true
+  | must_monomorphize (Mangled _) = true
+  | must_monomorphize _ = false
+
 fun run_atp auto name
         ({exec, required_execs, arguments, slices, proof_delims, known_failures,
           use_conjecture_for_hypotheses, ...} : atp_config)
@@ -414,7 +418,8 @@
                         |> not (null blacklist)
                            ? filter_out (member (op =) blacklist o fst
                                          o untranslated_fact)
-                        |> monomorphize ? monomorphize_facts
+                        |> (monomorphize orelse must_monomorphize type_sys)
+                           ? monomorphize_facts
                         |> map (atp_translated_fact ctxt)
                 val real_ms = Real.fromInt o Time.toMilliseconds
                 val slice_timeout =