merged

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 17:44:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 19:03:49 2012 +0100
@@ -42,6 +42,7 @@
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
 struct
 
+open ATP_Util
 open ATP_Problem_Generate
 open Metis_Tactic
 open Sledgehammer_Util
@@ -216,16 +217,19 @@
     fun is_boring_bool t =
       not (exists_subterm is_interesting_subterm t) orelse
       exists_type (exists_subtype (curry (op =) @{typ prop})) t
-    fun is_boring_prop (@{const Trueprop} $ t) = is_boring_bool t
-      | is_boring_prop (@{const "==>"} $ t $ u) =
-        is_boring_prop t andalso is_boring_prop u
-      | is_boring_prop (Const (@{const_name all}, _) $ (Abs (_, _, t)) $ u) =
-        is_boring_prop t andalso is_boring_prop u
-      | is_boring_prop (Const (@{const_name "=="}, _) $ t $ u) =
+    fun is_boring_prop _ (@{const Trueprop} $ t) = is_boring_bool t
+      | is_boring_prop Ts (@{const "==>"} $ t $ u) =
+        is_boring_prop Ts t andalso is_boring_prop Ts u
+      | is_boring_prop Ts (Const (@{const_name all}, _) $ Abs (_, T, t)) =
+        is_boring_prop (T :: Ts) t
+      | is_boring_prop Ts ((t as Const (@{const_name all}, _)) $ u) =
+        is_boring_prop Ts (t $ eta_expand Ts u 1)
+      | is_boring_prop _ (Const (@{const_name "=="}, _) $ t $ u) =
         is_boring_bool t andalso is_boring_bool u
-      | is_boring_prop _ = true
+      | is_boring_prop _ _ = true
   in
-    is_boring_prop (prop_of th) andalso not (Thm.eq_thm_prop (@{thm ext}, th))
+    is_boring_prop [] (prop_of th) andalso
+    not (Thm.eq_thm_prop (@{thm ext}, th))
   end
 
 fun is_theorem_bad_for_atps ho_atp th =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 17:44:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Dec 12 19:03:49 2012 +0100
@@ -624,11 +624,11 @@
          (max_new_instances |> the_default best_max_new_instances)
   #> Config.put Monomorph.keep_partial_instances false
 
-fun suffix_for_mode Auto_Try = "_auto_try"
+fun suffix_for_mode Auto_Try = "_try"
   | suffix_for_mode Try = "_try"
   | suffix_for_mode Normal = ""
-  | suffix_for_mode MaSh = "_mash"
-  | suffix_for_mode Auto_Minimize = "_auto_min"
+  | suffix_for_mode MaSh = ""
+  | suffix_for_mode Auto_Minimize = "_min"
   | suffix_for_mode Minimize = "_min"
 
 (* Give the ATPs some slack before interrupting them the hard way. "z3_tptp" on