# HG changeset patch
# User blanchet
# Date 1307386566 -7200
# Node ID e1fdd27e0c988d96a53e2ff8a8ff6d66ec22f362
# Parent  050a03afe0241979e967fbf8b70ac83bc2f44536
generate less type information in polymorphic case

diff -r 050a03afe024 -r e1fdd27e0c98 src/HOL/Metis_Examples/Proxies.thy
--- a/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:56:06 2011 +0200
+++ b/src/HOL/Metis_Examples/Proxies.thy	Mon Jun 06 20:56:06 2011 +0200
@@ -58,7 +58,7 @@
 
 lemma "id (op =) x x"
 sledgehammer [type_sys = erased, expect = none] (id_apply)
-sledgehammer [type_sys = poly_tags?, expect = none] (id_apply) (* unfortunate *)
+sledgehammer [type_sys = poly_tags?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_tags, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds?, expect = some] (id_apply)
 sledgehammer [type_sys = poly_preds, expect = some] (id_apply)
diff -r 050a03afe024 -r e1fdd27e0c98 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:56:06 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jun 06 20:56:06 2011 +0200
@@ -1059,8 +1059,7 @@
           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
           fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
             {pred_sym = pred_sym andalso not bool_vars',
-             min_ary =
-               fold (fn T' => consider_var_arity T' T) types min_ary,
+             min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
              max_ary = max_ary, types = types}
           val fun_var_Ts' =
             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
@@ -1069,8 +1068,7 @@
              pointer_eq (fun_var_Ts', fun_var_Ts) then
             accum
           else
-            ((bool_vars', fun_var_Ts'),
-             Symtab.map (K repair_min_arity) sym_tab)
+            ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
         end
       else
         accum
@@ -1833,7 +1831,7 @@
       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_sys
                        |> map repair
     val lavish_nonmono_Ts =
-      if null nonmono_Ts orelse
+      if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
          polymorphism_of_type_sys type_sys <> Polymorphic then
         nonmono_Ts
       else