perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
it's a mistake to transform the elim rules too early because then we lose some info, e.g. "no_atp" attributes

--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -141,7 +141,6 @@
     hol_context -> bool -> styp -> int -> styp
   val sel_no_from_name : string -> int
   val close_form : term -> term
-  val eta_expand : typ list -> term -> int -> term
   val distinctness_formula : typ -> term list -> term
   val register_frac_type :
     string -> (string * string) list -> morphism -> Context.generic
@@ -919,14 +918,6 @@
       | aux zs t = close_up zs (Term.add_vars t zs) t
   in aux [] end
 
-fun eta_expand _ t 0 = t
-  | eta_expand Ts (Abs (s, T, t')) n =
-    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
-  | eta_expand Ts t n =
-    fold_rev (curry3 Abs ("x" ^ nat_subscript n))
-             (List.take (binder_types (fastype_of1 (Ts, t)), n))
-             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
-
 fun distinctness_formula T =
   all_distinct_unordered_pairs_of
   #> map (fn (t1, t2) => @{const Not} $ (HOLogic.eq_const T $ t1 $ t2))

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -52,6 +52,7 @@
   val pretty_serial_commas : string -> Pretty.T list -> Pretty.T list
   val parse_bool_option : bool -> string -> string -> bool option
   val parse_time_option : string -> string -> Time.time option
+  val nat_subscript : int -> string
   val flip_polarity : polarity -> polarity
   val prop_T : typ
   val bool_T : typ
@@ -67,7 +68,7 @@
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> string * typ -> term -> term
   val varify_type : Proof.context -> typ -> typ
-  val nat_subscript : int -> string
+  val eta_expand : typ list -> term -> int -> term
   val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
   val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
   val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b
@@ -237,6 +238,18 @@
 val parse_bool_option = Sledgehammer_Util.parse_bool_option
 val parse_time_option = Sledgehammer_Util.parse_time_option
 
+val i_subscript = implode o map (prefix "\<^isub>") o explode
+fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
+fun nat_subscript n =
+  let val s = signed_string_of_int n in
+    if print_mode_active Symbol.xsymbolsN then
+      (* cheap trick to ensure proper alphanumeric ordering for one- and
+         two-digit numbers *)
+      (if n <= 9 then be_subscript else i_subscript) s
+    else
+      s
+  end
+
 fun flip_polarity Pos = Neg
   | flip_polarity Neg = Pos
   | flip_polarity Neut = Neut
@@ -258,17 +271,7 @@
   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
   |> snd |> the_single |> dest_Const |> snd
 
-val i_subscript = implode o map (prefix "\<^isub>") o explode
-fun be_subscript s = "\<^bsub>" ^ s ^ "\<^esub>"
-fun nat_subscript n =
-  let val s = signed_string_of_int n in
-    if print_mode_active Symbol.xsymbolsN then
-      (* cheap trick to ensure proper alphanumeric ordering for one- and
-         two-digit numbers *)
-      (if n <= 9 then be_subscript else i_subscript) s
-    else
-      s
-  end
+val eta_expand = Sledgehammer_Util.eta_expand
 
 fun time_limit NONE = I
   | time_limit (SOME delay) = TimeLimit.timeLimit delay

--- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -7,7 +7,6 @@
 
 signature CLAUSIFIER =
 sig
-  val transform_elim_theorem : thm -> thm
   val extensionalize_theorem : thm -> thm
   val introduce_combinators_in_cterm : cterm -> thm
   val introduce_combinators_in_theorem : thm -> thm
@@ -25,7 +24,7 @@
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to False. (Cf. "transform_elim_term" in
-   "ATP_Systems".) *)
+   "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   case concl_of th of    (*conclusion variable*)
        @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
@@ -78,10 +77,6 @@
 
 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
 
-(*Returns the vars of a theorem*)
-fun vars_of_thm th =
-  map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
-
 val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
 
 (* Removes the lambdas from an equation of the form "t = (%x. u)".

--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -775,9 +775,6 @@
              [])
   end;
 
-val type_has_top_sort =
-  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
-
 (* Extensionalize "th", because that makes sense and that's what Sledgehammer
    does, but also keep an unextensionalized version of "th" for backward
    compatibility. *)
@@ -794,6 +791,9 @@
   #> map Clausifier.introduce_combinators_in_theorem
   #> Meson.finish_cnf
 
+val type_has_top_sort =
+  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
+
 fun generic_metis_tac mode ctxt ths i st0 =
   let
     val _ = trace_msg (fn () =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -23,6 +23,8 @@
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
 struct
 
+open Sledgehammer_Util
+
 val trace = Unsynchronized.ref false
 fun trace_msg msg = if !trace then tracing (msg ()) else ()
 
@@ -43,7 +45,7 @@
     val name = Facts.string_of_ref xref
                |> forall (member Thm.eq_thm chained_ths) ths
                   ? prefix chained_prefix
-  in (name, ths |> map Clausifier.transform_elim_theorem) end
+  in (name, ths) end
 
 
 (***************************************************************)
@@ -420,7 +422,7 @@
 val exists_sledgehammer_const =
   exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
 
-fun is_strange_thm th =
+fun is_strange_theorem th =
   case head_of (concl_of th) of
       Const (a, _) => (a <> @{const_name Trueprop} andalso
                        a <> @{const_name "=="})
@@ -486,13 +488,15 @@
    are omitted. *)
 fun is_dangerous_term full_types t =
   not full_types andalso
-  (has_bound_or_var_of_type dangerous_types t orelse is_exhaustive_finite t)
+  ((has_bound_or_var_of_type dangerous_types t andalso
+    has_bound_or_var_of_type dangerous_types (transform_elim_term t))
+   orelse is_exhaustive_finite t)
 
 fun is_theorem_bad_for_atps full_types thm =
   let val t = prop_of thm in
     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
     is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
-    is_strange_thm thm
+    is_strange_theorem thm
   end
 
 fun all_name_thms_pairs ctxt full_types add_thms chained_ths =
@@ -525,8 +529,7 @@
             val name1 = Facts.extern facts name;
             val name2 = Name_Space.extern full_space name;
             val ths =
-              ths0 |> map Clausifier.transform_elim_theorem
-                   |> filter ((not o is_theorem_bad_for_atps full_types) orf
+              ths0 |> filter ((not o is_theorem_bad_for_atps full_types) orf
                               member Thm.eq_thm add_thms)
             val name' =
               case find_first check_thms [name1, name2, name] of
@@ -538,7 +541,7 @@
                                          (prop_of th) ^ "`")
                     |> space_implode " "
           in
-            cons (name' |> forall (member Thm.eq_thm chained_ths) ths
+            cons (name' |> forall (member Thm.eq_thm chained_ths) ths0
                            ? prefix chained_prefix, ths)
           end)
   in

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -119,8 +119,12 @@
             @{const Not} $ t1 => @{const Not} $ aux Ts t1
           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
             t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name All}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
             t0 $ Abs (s, T, aux (T :: Ts) t')
+          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
+            aux Ts (t0 $ eta_expand Ts t1 1)
           | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
           | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
@@ -175,8 +179,10 @@
   let
     val thy = ProofContext.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
+              |> transform_elim_term
               |> atomize_term
-    val t = t |> fastype_of t = HOLogic.boolT ? HOLogic.mk_Trueprop
+    val need_trueprop = (fastype_of t = HOLogic.boolT)
+    val t = t |> need_trueprop ? HOLogic.mk_Trueprop
               |> extensionalize_term
               |> presimp ? presimplify_term thy
               |> perhaps (try (HOLogic.dest_Trueprop))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Aug 23 14:51:56 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Aug 23 14:54:17 2010 +0200
@@ -16,6 +16,8 @@
   val unyxml : string -> string
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
+  val eta_expand : typ list -> term -> int -> term
+  val transform_elim_term : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val subgoal_count : Proof.state -> int
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
@@ -107,6 +109,25 @@
       | NONE => raise TERM ("monomorphic_term: uninstanitated schematic type \
                             \variable", [t]))) t
 
+fun eta_expand _ t 0 = t
+  | eta_expand Ts (Abs (s, T, t')) n =
+    Abs (s, T, eta_expand (T :: Ts) t' (n - 1))
+  | eta_expand Ts t n =
+    fold_rev (fn T => fn t' => Abs ("x" ^ nat_subscript n, T, t'))
+             (List.take (binder_types (fastype_of1 (Ts, t)), n))
+             (list_comb (incr_boundvars n t, map Bound (n - 1 downto 0)))
+
+(* Converts an elim-rule into an equivalent theorem that does not have the
+   predicate variable. Leaves other theorems unchanged. We simply instantiate
+   the conclusion variable to False. (Cf. "transform_elim_theorem" in
+   "Clausifier".) *)
+fun transform_elim_term t =
+  case Logic.strip_imp_concl t of
+    @{const Trueprop} $ Var (z, @{typ bool}) =>
+    subst_Vars [(z, @{const False})] t
+  | Var (z, @{typ prop}) => subst_Vars [(z, @{prop False})] t
+  | _ => t
+
 fun specialize_type thy (s, T) t =
   let
     fun subst_for (Const (s', T')) =