merged
authorhaftmann
Sun, 17 Jul 2011 20:23:39 +0200
changeset 43869 58be172c6ca4
parent 43864 58a7b3fdc193 (diff)
parent 43868 9684251c7ec1 (current diff)
child 43870 92129f505125
merged
--- a/src/HOL/TPTP/atp_export.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -160,7 +160,8 @@
       facts
       |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
       |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
-                             combinatorsN false true [] @{prop False}
+                             (rpair [] o map (introduce_combinators ctxt))
+                             false true [] @{prop False}
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -251,34 +251,6 @@
 
 (** Hard-core proof reconstruction: structured Isar proofs **)
 
-(* Simple simplifications to ensure that sort annotations don't leave a trail of
-   spurious "True"s. *)
-fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
-    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
-  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
-    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
-  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
-  | s_not (@{const HOL.conj} $ t1 $ t2) =
-    @{const HOL.disj} $ s_not t1 $ s_not t2
-  | s_not (@{const HOL.disj} $ t1 $ t2) =
-    @{const HOL.conj} $ s_not t1 $ s_not t2
-  | s_not (@{const False}) = @{const True}
-  | s_not (@{const True}) = @{const False}
-  | s_not (@{const Not} $ t) = t
-  | s_not t = @{const Not} $ t
-fun s_conj (@{const True}, t2) = t2
-  | s_conj (t1, @{const True}) = t1
-  | s_conj p = HOLogic.mk_conj p
-fun s_disj (@{const False}, t2) = t2
-  | s_disj (t1, @{const False}) = t1
-  | s_disj p = HOLogic.mk_disj p
-fun s_imp (@{const True}, t2) = t2
-  | s_imp (t1, @{const False}) = s_not t1
-  | s_imp p = HOLogic.mk_imp p
-fun s_iff (@{const True}, t2) = t2
-  | s_iff (t1, @{const True}) = t1
-  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
-
 fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
 fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
 
--- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -3,7 +3,7 @@
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
 
-Translation of HOL to FOL for Sledgehammer.
+Translation of HOL to FOL for Metis and Sledgehammer.
 *)
 
 signature ATP_TRANSLATE =
@@ -31,11 +31,6 @@
     Preds of polymorphism * type_level * type_heaviness |
     Tags of polymorphism * type_level * type_heaviness
 
-  val concealed_lambdasN : string
-  val lambda_liftingN : string
-  val combinatorsN : string
-  val lambdasN : string
-  val smartN : string
   val bound_var_prefix : string
   val schematic_var_prefix : string
   val fixed_var_prefix : string
@@ -93,10 +88,12 @@
   val unmangled_const_name : string -> string
   val helper_table : ((string * bool) * thm list) list
   val factsN : string
+  val conceal_lambdas : Proof.context -> term -> term
+  val introduce_combinators : Proof.context -> term -> term
   val prepare_atp_problem :
     Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
-    -> bool -> string -> bool -> bool -> term list -> term
-    -> ((string * locality) * term) list
+    -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
+    -> term -> ((string * locality) * term) list
     -> string problem * string Symtab.table * int * int
        * (string * locality) list vector * int list * int Symtab.table
   val atp_problem_weights : string problem -> (string * real) list
@@ -110,12 +107,6 @@
 
 type name = string * string
 
-val concealed_lambdasN = "concealed_lambdas"
-val lambda_liftingN = "lambda_lifting"
-val combinatorsN = "combinators"
-val lambdasN = "lambdas"
-val smartN = "smart"
-
 val generate_info = false (* experimental *)
 
 fun isabelle_info s =
@@ -129,15 +120,13 @@
 val bound_var_prefix = "B_"
 val schematic_var_prefix = "V_"
 val fixed_var_prefix = "v_"
-
 val tvar_prefix = "T_"
 val tfree_prefix = "t_"
-
 val const_prefix = "c_"
 val type_const_prefix = "tc_"
 val class_prefix = "cl_"
 
-val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
+val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
 
@@ -152,6 +141,7 @@
 val arity_clause_prefix = "arity_"
 val tfree_clause_prefix = "tfree_"
 
+val lambda_fact_prefix = "ATP.lambda_"
 val typed_helper_suffix = "_T"
 val untyped_helper_suffix = "_U"
 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
@@ -167,9 +157,9 @@
 val prefixed_type_tag_name = const_prefix ^ type_tag_name
 
 (* Freshness almost guaranteed! *)
-val sledgehammer_weak_prefix = "Sledgehammer:"
+val atp_weak_prefix = "ATP:"
 
-val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
+val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
 
 (*Escaping of special characters.
   Alphanumeric characters are left unchanged.
@@ -456,21 +446,22 @@
 fun make_class_rel_clauses thy subs supers =
   map make_class_rel_clause (class_pairs thy subs supers)
 
-datatype combterm =
-  CombConst of name * typ * typ list |
-  CombVar of name * typ |
-  CombApp of combterm * combterm |
-  CombAbs of (name * typ) * combterm
+(* intermediate terms *)
+datatype iterm =
+  IConst of name * typ * typ list |
+  IVar of name * typ |
+  IApp of iterm * iterm |
+  IAbs of (name * typ) * iterm
 
-fun combtyp_of (CombConst (_, T, _)) = T
-  | combtyp_of (CombVar (_, T)) = T
-  | combtyp_of (CombApp (t1, _)) = snd (dest_funT (combtyp_of t1))
-  | combtyp_of (CombAbs ((_, T), tm)) = T --> combtyp_of tm
+fun ityp_of (IConst (_, T, _)) = T
+  | ityp_of (IVar (_, T)) = T
+  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
+  | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
 
 (*gets the head of a combinator application, along with the list of arguments*)
-fun strip_combterm_comb u =
+fun strip_iterm_comb u =
   let
-    fun stripc (CombApp (t, u), ts) = stripc (t, u :: ts)
+    fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
       | stripc x = x
   in stripc (u, []) end
 
@@ -480,42 +471,41 @@
   [new_skolem_const_prefix, s, string_of_int num_T_args]
   |> space_implode Long_Name.separator
 
-(* Converts a term (with combinators) into a combterm. Also accumulates sort
-   infomation. *)
-fun combterm_from_term thy bs (P $ Q) =
+(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
+   Also accumulates sort infomation. *)
+fun iterm_from_term thy bs (P $ Q) =
     let
-      val (P', P_atomics_Ts) = combterm_from_term thy bs P
-      val (Q', Q_atomics_Ts) = combterm_from_term thy bs Q
-    in (CombApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
-  | combterm_from_term thy _ (Const (c, T)) =
+      val (P', P_atomics_Ts) = iterm_from_term thy bs P
+      val (Q', Q_atomics_Ts) = iterm_from_term thy bs Q
+    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
+  | iterm_from_term thy _ (Const (c, T)) =
     let
       val tvar_list =
         (if String.isPrefix old_skolem_const_prefix c then
            [] |> Term.add_tvarsT T |> map TVar
          else
            (c, T) |> Sign.const_typargs thy)
-      val c' = CombConst (`make_fixed_const c, T, tvar_list)
+      val c' = IConst (`make_fixed_const c, T, tvar_list)
     in (c', atyps_of T) end
-  | combterm_from_term _ _ (Free (v, T)) =
-    (CombConst (`make_fixed_var v, T, []), atyps_of T)
-  | combterm_from_term _ _ (Var (v as (s, _), T)) =
+  | iterm_from_term _ _ (Free (v, T)) =
+    (IConst (`make_fixed_var v, T, []), atyps_of T)
+  | iterm_from_term _ _ (Var (v as (s, _), T)) =
     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
        let
          val Ts = T |> strip_type |> swap |> op ::
          val s' = new_skolem_const_name s (length Ts)
-       in CombConst (`make_fixed_const s', T, Ts) end
+       in IConst (`make_fixed_const s', T, Ts) end
      else
-       CombVar ((make_schematic_var v, s), T), atyps_of T)
-  | combterm_from_term _ bs (Bound j) =
-    nth bs j
-    |> (fn (s, T) => (CombConst (`make_bound_var s, T, []), atyps_of T))
-  | combterm_from_term thy bs (Abs (s, T, t)) =
+       IVar ((make_schematic_var v, s), T), atyps_of T)
+  | iterm_from_term _ bs (Bound j) =
+    nth bs j |> (fn (s, T) => (IConst (`make_bound_var s, T, []), atyps_of T))
+  | iterm_from_term thy bs (Abs (s, T, t)) =
     let
       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
       val s = vary s
-      val (tm, atomic_Ts) = combterm_from_term thy ((s, T) :: bs) t
+      val (tm, atomic_Ts) = iterm_from_term thy ((s, T) :: bs) t
     in
-      (CombAbs ((`make_bound_var s, T), tm),
+      (IAbs ((`make_bound_var s, T), tm),
        union (op =) atomic_Ts (atyps_of T))
     end
 
@@ -630,15 +620,15 @@
   {name : string,
    locality : locality,
    kind : formula_kind,
-   combformula : (name, typ, combterm) formula,
+   iformula : (name, typ, iterm) formula,
    atomic_types : typ list}
 
-fun update_combformula f ({name, locality, kind, combformula, atomic_types}
-                          : translated_formula) =
-  {name = name, locality = locality, kind = kind, combformula = f combformula,
+fun update_iformula f ({name, locality, kind, iformula, atomic_types}
+                       : translated_formula) =
+  {name = name, locality = locality, kind = kind, iformula = f iformula,
    atomic_types = atomic_types} : translated_formula
 
-fun fact_lift f ({combformula, ...} : translated_formula) = f combformula
+fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
 
 val type_instance = Sign.typ_instance o Proof_Context.theory_of
 
@@ -721,11 +711,11 @@
                       |> filter_out (member (op =) bounds o fst))
   in mk_aquant AForall (formula_vars [] phi []) phi end
 
-fun combterm_vars (CombApp (tm1, tm2)) = fold combterm_vars [tm1, tm2]
-  | combterm_vars (CombConst _) = I
-  | combterm_vars (CombVar (name, T)) = insert (op =) (name, SOME T)
-  | combterm_vars (CombAbs (_, tm)) = combterm_vars tm
-fun close_combformula_universally phi = close_universally combterm_vars phi
+fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
+  | iterm_vars (IConst _) = I
+  | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
+  | iterm_vars (IAbs (_, tm)) = iterm_vars tm
+fun close_iformula_universally phi = close_universally iterm_vars phi
 
 fun term_vars bounds (ATerm (name as (s, _), tms)) =
     (is_tptp_variable s andalso not (member (op =) bounds name))
@@ -825,9 +815,9 @@
 
 fun introduce_proxies type_enc =
   let
-    fun intro top_level (CombApp (tm1, tm2)) =
-        CombApp (intro top_level tm1, intro false tm2)
-      | intro top_level (CombConst (name as (s, _), T, T_args)) =
+    fun intro top_level (IApp (tm1, tm2)) =
+        IApp (intro top_level tm1, intro false tm2)
+      | intro top_level (IConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
            SOME proxy_base =>
            if top_level orelse is_type_enc_higher_order type_enc then
@@ -847,15 +837,15 @@
            else
              (proxy_base |>> prefix const_prefix, T_args)
           | NONE => (name, T_args))
-        |> (fn (name, T_args) => CombConst (name, T, T_args))
-      | intro _ (CombAbs (bound, tm)) = CombAbs (bound, intro false tm)
+        |> (fn (name, T_args) => IConst (name, T, T_args))
+      | intro _ (IAbs (bound, tm)) = IAbs (bound, intro false tm)
       | intro _ tm = tm
   in intro true end
 
-fun combformula_from_prop thy type_enc eq_as_iff =
+fun iformula_from_prop thy type_enc eq_as_iff =
   let
     fun do_term bs t atomic_types =
-      combterm_from_term thy bs (Envir.eta_contract t)
+      iterm_from_term thy bs (Envir.eta_contract t)
       |>> (introduce_proxies type_enc #> AAtom)
       ||> union (op =) atomic_types
     fun do_quant bs q s T t' =
@@ -888,7 +878,7 @@
             #> Meson.presimplify ctxt
             #> prop_of)
 
-fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
+fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
 fun conceal_bounds Ts t =
   subst_bounds (map (Free o apfst concealed_bound_name)
                     (0 upto length Ts - 1 ~~ Ts), t)
@@ -909,14 +899,7 @@
   else
     t
 
-fun conceal_lambdas Ts (t1 $ t2) = conceal_lambdas Ts t1 $ conceal_lambdas Ts t2
-  | conceal_lambdas Ts (Abs (_, T, t)) =
-    (* slightly unsound because of hash collisions *)
-    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
-          T --> fastype_of1 (Ts, t))
-  | conceal_lambdas _ t = t
-
-fun process_abstractions_in_term ctxt lambda_trans kind t =
+fun simple_translate_lambdas do_lambdas ctxt t =
   let val thy = Proof_Context.theory_of ctxt in
     if Meson.is_fol_term thy t then
       t
@@ -940,34 +923,45 @@
               $ t1 $ t2 =>
             t0 $ aux Ts t1 $ aux Ts t2
           | _ =>
-            if not (exists_subterm (fn Abs _ => true | _ => false) t) then
-              t
-            else
-              let val t = t |> Envir.eta_contract in
-                if lambda_trans = concealed_lambdasN then
-                  t |> conceal_lambdas []
-                else if lambda_trans = lambda_liftingN then
-                  t (* TODO: implement *)
-                else if lambda_trans = combinatorsN then
-                  t |> conceal_bounds Ts
-                    |> cterm_of thy
-                    |> Meson_Clausify.introduce_combinators_in_cterm
-                    |> prop_of |> Logic.dest_equals |> snd
-                    |> reveal_bounds Ts
-                else if lambda_trans = lambdasN then
-                  t
-                else
-                  error ("Unknown lambda translation method: " ^
-                         quote lambda_trans ^ ".")
-              end
+            if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
+            else t |> Envir.eta_contract |> do_lambdas ctxt Ts
         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
-      handle THM _ =>
-             (* A type variable of sort "{}" will make abstraction fail. *)
-             if kind = Conjecture then HOLogic.false_const
-             else HOLogic.true_const
   end
 
+fun do_conceal_lambdas Ts (t1 $ t2) =
+    do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
+  | do_conceal_lambdas Ts (Abs (_, T, t)) =
+    (* slightly unsound because of hash collisions *)
+    Free (concealed_lambda_prefix ^ string_of_int (hash_term t),
+          T --> fastype_of1 (Ts, t))
+  | do_conceal_lambdas _ t = t
+val conceal_lambdas = simple_translate_lambdas (K do_conceal_lambdas)
+
+fun do_introduce_combinators ctxt Ts t =
+  let val thy = Proof_Context.theory_of ctxt in
+    t |> not (Meson.is_fol_term thy t)
+         ? (conceal_bounds Ts
+            #> cterm_of thy
+            #> Meson_Clausify.introduce_combinators_in_cterm
+            #> prop_of #> Logic.dest_equals #> snd
+            #> reveal_bounds Ts)
+  end
+  (* A type variable of sort "{}" will make abstraction fail. *)
+  handle THM _ => t |> do_conceal_lambdas Ts
+val introduce_combinators = simple_translate_lambdas do_introduce_combinators
+
+fun preprocess_abstractions_in_terms trans_lambdas facts =
+  let
+    val (facts, lambda_ts) =
+      facts |> map (snd o snd) |> trans_lambdas 
+            |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
+    val lambda_facts =
+      map2 (fn t => fn j =>
+               ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
+           lambda_ts (1 upto length lambda_ts)
+  in (facts, lambda_facts) end
+
 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
 fun freeze_term t =
@@ -975,11 +969,11 @@
     fun aux (t $ u) = aux t $ aux u
       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
       | aux (Var ((s, i), T)) =
-        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
+        Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
       | aux t = t
   in t |> exists_subterm is_Var t ? aux end
 
-fun preprocess_prop ctxt lambda_trans presimp_consts kind t =
+fun presimp_prop ctxt presimp_consts t =
   let
     val thy = Proof_Context.theory_of ctxt
     val t = t |> Envir.beta_eta_contract
@@ -992,54 +986,36 @@
       |> extensionalize_term ctxt
       |> presimplify_term ctxt presimp_consts
       |> perhaps (try (HOLogic.dest_Trueprop))
-      |> process_abstractions_in_term ctxt lambda_trans kind
   end
 
 (* making fact and conjecture formulas *)
 fun make_formula thy type_enc eq_as_iff name loc kind t =
   let
-    val (combformula, atomic_types) =
-      combformula_from_prop thy type_enc eq_as_iff t []
+    val (iformula, atomic_types) =
+      iformula_from_prop thy type_enc eq_as_iff t []
   in
-    {name = name, locality = loc, kind = kind, combformula = combformula,
+    {name = name, locality = loc, kind = kind, iformula = iformula,
      atomic_types = atomic_types}
   end
 
-fun make_fact ctxt format type_enc lambda_trans eq_as_iff preproc presimp_consts
-              ((name, loc), t) =
+fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
   let val thy = Proof_Context.theory_of ctxt in
-    case t |> preproc ? preprocess_prop ctxt lambda_trans presimp_consts Axiom
-           |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
+    case t |> make_formula thy type_enc (eq_as_iff andalso format <> CNF) name
                            loc Axiom of
-      formula as {combformula = AAtom (CombConst ((s, _), _, _)), ...} =>
+      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
       if s = tptp_true then NONE else SOME formula
     | formula => SOME formula
   end
 
-fun make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
-                    presimp_consts ts =
+fun make_conjecture ctxt format type_enc ps =
   let
     val thy = Proof_Context.theory_of ctxt
-    val last = length ts - 1
+    val last = length ps - 1
   in
-    map2 (fn j => fn t =>
-             let
-               val (kind, maybe_negate) =
-                 if j = last then
-                   (Conjecture, I)
-                 else
-                   (prem_kind,
-                    if prem_kind = Conjecture then update_combformula mk_anot
-                    else I)
-              in
-                t |> preproc ?
-                     (preprocess_prop ctxt lambda_trans presimp_consts kind
-                      #> freeze_term)
-                  |> make_formula thy type_enc (format <> CNF) (string_of_int j)
-                                  Local kind
-                  |> maybe_negate
-              end)
-         (0 upto last) ts
+    map2 (fn j => fn ((name, loc), (kind, t)) =>
+             t |> make_formula thy type_enc (format <> CNF) name loc kind
+               |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
+         (0 upto last) ps
   end
 
 (** Finite and infinite type inference **)
@@ -1066,9 +1042,9 @@
     should_encode_type ctxt nonmono_Ts level T
   | should_predicate_on_type _ _ _ _ _ = false
 
-fun is_var_or_bound_var (CombConst ((s, _), _, _)) =
+fun is_var_or_bound_var (IConst ((s, _), _, _)) =
     String.isPrefix bound_var_prefix s
-  | is_var_or_bound_var (CombVar _) = true
+  | is_var_or_bound_var (IVar _) = true
   | is_var_or_bound_var _ = false
 
 datatype tag_site =
@@ -1108,7 +1084,7 @@
 type sym_info =
   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
 
-fun add_combterm_syms_to_table ctxt explicit_apply =
+fun add_iterm_syms_to_table ctxt explicit_apply =
   let
     fun consider_var_arity const_T var_T max_ary =
       let
@@ -1140,9 +1116,9 @@
       else
         accum
     fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
-      let val (head, args) = strip_combterm_comb tm in
+      let val (head, args) = strip_iterm_comb tm in
         (case head of
-           CombConst ((s, _), T, _) =>
+           IConst ((s, _), T, _) =>
            if String.isPrefix bound_var_prefix s then
              add_var_or_bound_var T accum
            else
@@ -1182,16 +1158,15 @@
                                       sym_tab
                   end)
              end
-         | CombVar (_, T) => add_var_or_bound_var T accum
-         | CombAbs ((_, T), tm) =>
-           accum |> add_var_or_bound_var T |> add false tm
+         | IVar (_, T) => add_var_or_bound_var T accum
+         | IAbs ((_, T), tm) => accum |> add_var_or_bound_var T |> add false tm
          | _ => accum)
         |> fold (add false) args
       end
   in add true end
 fun add_fact_syms_to_table ctxt explicit_apply =
   fact_lift (formula_fold NONE
-                          (K (add_combterm_syms_to_table ctxt explicit_apply)))
+                          (K (add_iterm_syms_to_table ctxt explicit_apply)))
 
 val default_sym_tab_entries : (string * sym_info) list =
   (prefixed_predicator_name,
@@ -1231,33 +1206,32 @@
   | NONE => false
 
 val predicator_combconst =
-  CombConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
-fun predicator tm = CombApp (predicator_combconst, tm)
+  IConst (`make_fixed_const predicator_name, @{typ "bool => bool"}, [])
+fun predicator tm = IApp (predicator_combconst, tm)
 
-fun introduce_predicators_in_combterm sym_tab tm =
-  case strip_combterm_comb tm of
-    (CombConst ((s, _), _, _), _) =>
+fun introduce_predicators_in_iterm sym_tab tm =
+  case strip_iterm_comb tm of
+    (IConst ((s, _), _, _), _) =>
     if is_pred_sym sym_tab s then tm else predicator tm
   | _ => predicator tm
 
-fun list_app head args = fold (curry (CombApp o swap)) args head
+fun list_app head args = fold (curry (IApp o swap)) args head
 
 val app_op = `make_fixed_const app_op_name
 
 fun explicit_app arg head =
   let
-    val head_T = combtyp_of head
+    val head_T = ityp_of head
     val (arg_T, res_T) = dest_funT head_T
-    val explicit_app =
-      CombConst (app_op, head_T --> head_T, [arg_T, res_T])
+    val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
   in list_app explicit_app [head, arg] end
 fun list_explicit_app head args = fold explicit_app args head
 
-fun introduce_explicit_apps_in_combterm sym_tab =
+fun introduce_explicit_apps_in_iterm sym_tab =
   let
     fun aux tm =
-      case strip_combterm_comb tm of
-        (head as CombConst ((s, _), _, _), args) =>
+      case strip_iterm_comb tm of
+        (head as IConst ((s, _), _, _), args) =>
         args |> map aux
              |> chop (min_arity_of sym_tab s)
              |>> list_app head
@@ -1291,12 +1265,11 @@
     end
     handle TYPE _ => T_args
 
-fun enforce_type_arg_policy_in_combterm ctxt format type_enc =
+fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
   let
     val thy = Proof_Context.theory_of ctxt
-    fun aux arity (CombApp (tm1, tm2)) =
-        CombApp (aux (arity + 1) tm1, aux 0 tm2)
-      | aux arity (CombConst (name as (s, _), T, T_args)) =
+    fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
+      | aux arity (IConst (name as (s, _), T, T_args)) =
         (case strip_prefix_and_unascii const_prefix s of
            NONE => (name, T_args)
          | SOME s'' =>
@@ -1313,19 +1286,18 @@
                                    name, [])
              | No_Type_Args => (name, [])
            end)
-        |> (fn (name, T_args) => CombConst (name, T, T_args))
-      | aux _ (CombAbs (bound, tm)) = CombAbs (bound, aux 0 tm)
+        |> (fn (name, T_args) => IConst (name, T, T_args))
+      | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
       | aux _ tm = tm
   in aux 0 end
 
-fun repair_combterm ctxt format type_enc sym_tab =
+fun repair_iterm ctxt format type_enc sym_tab =
   not (is_type_enc_higher_order type_enc)
-  ? (introduce_explicit_apps_in_combterm sym_tab
-     #> introduce_predicators_in_combterm sym_tab)
-  #> enforce_type_arg_policy_in_combterm ctxt format type_enc
+  ? (introduce_explicit_apps_in_iterm sym_tab
+     #> introduce_predicators_in_iterm sym_tab)
+  #> enforce_type_arg_policy_in_iterm ctxt format type_enc
 fun repair_fact ctxt format type_enc sym_tab =
-  update_combformula (formula_map
-      (repair_combterm ctxt format type_enc sym_tab))
+  update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
 
 (** Helper facts **)
 
@@ -1381,8 +1353,7 @@
   level_of_type_enc type_enc <> No_Types andalso
   not (null (Term.hidden_polymorphism t))
 
-fun helper_facts_for_sym ctxt format type_enc lambda_trans
-                         (s, {types, ...} : sym_info) =
+fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
   case strip_prefix_and_unascii const_prefix s of
     SOME mangled_s =>
     let
@@ -1403,8 +1374,7 @@
             [t]
         end
         |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
-      val make_facts =
-        map_filter (make_fact ctxt format type_enc lambda_trans false false [])
+      val make_facts = map_filter (make_fact ctxt format type_enc false)
       val fairly_sound = is_type_enc_fairly_sound type_enc
     in
       helper_table
@@ -1418,10 +1388,9 @@
                     |> make_facts)
     end
   | NONE => []
-fun helper_facts_for_sym_table ctxt format type_enc lambda_trans sym_tab =
-  Symtab.fold_rev (append
-                   o helper_facts_for_sym ctxt format type_enc lambda_trans)
-                  sym_tab []
+fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
+  Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
+                  []
 
 (***************************************************************)
 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
@@ -1461,38 +1430,50 @@
 fun type_constrs_of_terms thy ts =
   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
 
-fun translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                        hyp_ts concl_t facts =
   let
     val thy = Proof_Context.theory_of ctxt
+    val presimp_consts = Meson.presimplified_consts ctxt
     val fact_ts = facts |> map snd
-    val presimp_consts = Meson.presimplified_consts ctxt
-    val make_fact =
-      make_fact ctxt format type_enc lambda_trans true preproc presimp_consts
-    val (facts, fact_names) =
-      facts |> map (fn (name, t) => (name, t) |> make_fact |> rpair name)
-            |> map_filter (try (apfst the))
-            |> ListPair.unzip
     (* Remove existing facts from the conjecture, as this can dramatically
        boost an ATP's performance (for some reason). *)
     val hyp_ts =
       hyp_ts
       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
-    val goal_t = Logic.list_implies (hyp_ts, concl_t)
-    val all_ts = goal_t :: fact_ts
+    val facts = facts |> map (apsnd (pair Axiom))
+    val conjs =
+      map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
+      |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
+    val ((conjs, facts), lambdas) =
+      if preproc then
+        conjs @ facts
+        |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
+        |> preprocess_abstractions_in_terms trans_lambdas
+        |>> chop (length conjs)
+        |>> apfst (map (apsnd (apsnd freeze_term)))
+      else
+        ((conjs, facts), [])
+    val conjs = conjs |> make_conjecture ctxt format type_enc
+    val (fact_names, facts) =
+      facts
+      |> map_filter (fn (name, (_, t)) =>
+                        make_fact ctxt format type_enc true (name, t)
+                        |> Option.map (pair name))
+      |> ListPair.unzip
+    val lambdas =
+      lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
+    val all_ts = concl_t :: hyp_ts @ fact_ts
     val subs = tfree_classes_of_terms all_ts
     val supers = tvar_classes_of_terms all_ts
     val tycons = type_constrs_of_terms thy all_ts
-    val conjs =
-      hyp_ts @ [concl_t]
-      |> make_conjecture ctxt format prem_kind type_enc lambda_trans preproc
-                         presimp_consts
-    val (supers', arity_clauses) =
+    val (supers, arity_clauses) =
       if level_of_type_enc type_enc = No_Types then ([], [])
       else make_arity_clauses thy tycons supers
-    val class_rel_clauses = make_class_rel_clauses thy subs supers'
+    val class_rel_clauses = make_class_rel_clauses thy subs supers
   in
-    (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
+    (fact_names |> map single,
+     (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
   end
 
 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
@@ -1504,9 +1485,9 @@
 
 val type_pred = `make_fixed_const type_pred_name
 
-fun type_pred_combterm ctxt format type_enc T tm =
-  CombApp (CombConst (type_pred, T --> @{typ bool}, [T])
-           |> enforce_type_arg_policy_in_combterm ctxt format type_enc, tm)
+fun type_pred_iterm ctxt format type_enc T tm =
+  IApp (IConst (type_pred, T --> @{typ bool}, [T])
+        |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
 
 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
@@ -1520,16 +1501,16 @@
   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
 
 fun tag_with_type ctxt format nonmono_Ts type_enc pos T tm =
-  CombConst (type_tag, T --> T, [T])
-  |> enforce_type_arg_policy_in_combterm ctxt format type_enc
-  |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+  IConst (type_tag, T --> T, [T])
+  |> enforce_type_arg_policy_in_iterm ctxt format type_enc
+  |> ho_term_from_iterm ctxt format nonmono_Ts type_enc (Top_Level pos)
   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
+and ho_term_from_iterm ctxt format nonmono_Ts type_enc =
   let
     fun aux site u =
       let
-        val (head, args) = strip_combterm_comb u
+        val (head, args) = strip_iterm_comb u
         val pos =
           case site of
             Top_Level pos => pos
@@ -1537,17 +1518,19 @@
           | Elsewhere => NONE
         val t =
           case head of
-            CombConst (name as (s, _), _, T_args) =>
+            IConst (name as (s, _), _, T_args) =>
             let
               val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
             in
               mk_aterm format type_enc name T_args (map (aux arg_site) args)
             end
-          | CombVar (name, _) => mk_aterm format type_enc name [] (map (aux Elsewhere) args)
-          | CombAbs ((name, T), tm) =>
-            AAbs ((name, ho_type_from_typ format type_enc true 0 T), aux Elsewhere tm)
-          | CombApp _ => raise Fail "impossible \"CombApp\""
-        val T = combtyp_of u
+          | IVar (name, _) =>
+            mk_aterm format type_enc name [] (map (aux Elsewhere) args)
+          | IAbs ((name, T), tm) =>
+            AAbs ((name, ho_type_from_typ format type_enc true 0 T),
+                  aux Elsewhere tm)
+          | IApp _ => raise Fail "impossible \"IApp\""
+        val T = ityp_of u
       in
         t |> (if should_tag_with_type ctxt nonmono_Ts type_enc site u T then
                 tag_with_type ctxt format nonmono_Ts type_enc pos T
@@ -1555,11 +1538,10 @@
                 I)
       end
   in aux end
-and formula_from_combformula ctxt format nonmono_Ts type_enc
-                             should_predicate_on_var =
+and formula_from_iformula ctxt format nonmono_Ts type_enc
+                          should_predicate_on_var =
   let
-    fun do_term pos =
-      ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
+    val do_term = ho_term_from_iterm ctxt format nonmono_Ts type_enc o Top_Level
     val do_bound_type =
       case type_enc of
         Simple_Types (_, level) =>
@@ -1569,8 +1551,8 @@
     fun do_out_of_bound_type pos phi universal (name, T) =
       if should_predicate_on_type ctxt nonmono_Ts type_enc
              (fn () => should_predicate_on_var pos phi universal name) T then
-        CombVar (name, T)
-        |> type_pred_combterm ctxt format type_enc T
+        IVar (name, T)
+        |> type_pred_iterm ctxt format type_enc T
         |> do_term pos |> AAtom |> SOME
       else
         NONE
@@ -1601,14 +1583,13 @@
    of monomorphization). The TPTP explicitly forbids name clashes, and some of
    the remote provers might care. *)
 fun formula_line_for_fact ctxt format prefix encode freshen pos nonmono_Ts
-        type_enc (j, {name, locality, kind, combformula, atomic_types}) =
-  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name,
-   kind,
-   combformula
-   |> close_combformula_universally
-   |> formula_from_combformula ctxt format nonmono_Ts type_enc
-                               should_predicate_on_var_in_formula
-                               (if pos then SOME true else NONE)
+        type_enc (j, {name, locality, kind, iformula, atomic_types}) =
+  (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
+   iformula
+   |> close_iformula_universally
+   |> formula_from_iformula ctxt format nonmono_Ts type_enc
+                            should_predicate_on_var_in_formula
+                            (if pos then SOME true else NONE)
    |> bound_tvars type_enc atomic_types
    |> close_formula_universally,
    NONE,
@@ -1643,11 +1624,11 @@
            |> close_formula_universally, isabelle_info introN, NONE)
 
 fun formula_line_for_conjecture ctxt format nonmono_Ts type_enc
-        ({name, kind, combformula, atomic_types, ...} : translated_formula) =
+        ({name, kind, iformula, atomic_types, ...} : translated_formula) =
   Formula (conjecture_prefix ^ name, kind,
-           formula_from_combformula ctxt format nonmono_Ts type_enc
+           formula_from_iformula ctxt format nonmono_Ts type_enc
                should_predicate_on_var_in_formula (SOME false)
-               (close_combformula_universally combformula)
+               (close_iformula_universally iformula)
            |> bound_tvars type_enc atomic_types
            |> close_formula_universally, NONE, NONE)
 
@@ -1675,10 +1656,10 @@
 
 fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
   let
-    fun add_combterm in_conj tm =
-      let val (head, args) = strip_combterm_comb tm in
+    fun add_iterm in_conj tm =
+      let val (head, args) = strip_iterm_comb tm in
         (case head of
-           CombConst ((s, s'), T, T_args) =>
+           IConst ((s, s'), T, T_args) =>
            let val pred_sym = is_pred_sym repaired_sym_tab s in
              if should_declare_sym type_enc pred_sym s then
                Symtab.map_default (s, [])
@@ -1687,12 +1668,11 @@
              else
                I
            end
-         | CombAbs (_, tm) => add_combterm in_conj tm
+         | IAbs (_, tm) => add_iterm in_conj tm
          | _ => I)
-        #> fold (add_combterm in_conj) args
+        #> fold (add_iterm in_conj) args
       end
-    fun add_fact in_conj =
-      fact_lift (formula_fold NONE (K (add_combterm in_conj)))
+    fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
   in
     Symtab.empty
     |> is_type_enc_fairly_sound type_enc
@@ -1701,10 +1681,9 @@
 
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    out with monotonicity" paper presented at CADE 2011. *)
-fun add_combterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
-  | add_combterm_nonmonotonic_types ctxt level sound locality _
-        (CombApp (CombApp (CombConst ((s, _), Type (_, [T, _]), _), tm1),
-                           tm2)) =
+fun add_iterm_nonmonotonic_types _ _ _ _ (SOME false) _ = I
+  | add_iterm_nonmonotonic_types ctxt level sound locality _
+        (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) =
     (is_tptp_equal s andalso exists is_var_or_bound_var [tm1, tm2] andalso
      (case level of
         Noninf_Nonmono_Types =>
@@ -1712,12 +1691,12 @@
         not (is_type_surely_infinite ctxt sound T)
       | Fin_Nonmono_Types => is_type_surely_finite ctxt false T
       | _ => true)) ? insert_type ctxt I (deep_freeze_type T)
-  | add_combterm_nonmonotonic_types _ _ _ _ _ _ = I
+  | add_iterm_nonmonotonic_types _ _ _ _ _ _ = I
 fun add_fact_nonmonotonic_types ctxt level sound
-        ({kind, locality, combformula, ...} : translated_formula) =
+        ({kind, locality, iformula, ...} : translated_formula) =
   formula_fold (SOME (kind <> Conjecture))
-               (add_combterm_nonmonotonic_types ctxt level sound locality)
-               combformula
+               (add_iterm_nonmonotonic_types ctxt level sound locality)
+               iformula
 fun nonmonotonic_types_for_facts ctxt type_enc sound facts =
   let val level = level_of_type_enc type_enc in
     if level = Noninf_Nonmono_Types orelse level = Fin_Nonmono_Types then
@@ -1754,7 +1733,7 @@
     val bound_names =
       1 upto num_args |> map (`I o make_bound_var o string_of_int)
     val bounds =
-      bound_names ~~ arg_Ts |> map (fn (name, T) => CombConst (name, T, []))
+      bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
     val sym_needs_arg_types = n > 1 orelse exists (curry (op =) dummyT) T_args
     fun should_keep_arg_type T =
       sym_needs_arg_types orelse
@@ -1764,12 +1743,12 @@
   in
     Formula (preds_sym_formula_prefix ^ s ^
              (if n > 1 then "_" ^ string_of_int j else ""), kind,
-             CombConst ((s, s'), T, T_args)
-             |> fold (curry (CombApp o swap)) bounds
-             |> type_pred_combterm ctxt format type_enc res_T
+             IConst ((s, s'), T, T_args)
+             |> fold (curry (IApp o swap)) bounds
+             |> type_pred_iterm ctxt format type_enc res_T
              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
-             |> formula_from_combformula ctxt format poly_nonmono_Ts type_enc
-                                         (K (K (K (K true)))) (SOME true)
+             |> formula_from_iformula ctxt format poly_nonmono_Ts type_enc
+                                      (K (K (K (K true)))) (SOME true)
              |> n > 1 ? bound_tvars type_enc (atyps_of T)
              |> close_formula_universally
              |> maybe_negate,
@@ -1903,11 +1882,11 @@
 val explicit_apply = NONE (* for experiments *)
 
 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc sound
-        exporter lambda_trans readable_names preproc hyp_ts concl_t facts =
+        exporter trans_lambdas readable_names preproc hyp_ts concl_t facts =
   let
     val (format, type_enc) = choose_format [format] type_enc
     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
-      translate_formulas ctxt format prem_kind type_enc lambda_trans preproc
+      translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
                          hyp_ts concl_t facts
     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
     val nonmono_Ts =
@@ -1917,9 +1896,8 @@
     val repaired_sym_tab =
       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
     val helpers =
-      repaired_sym_tab
-      |> helper_facts_for_sym_table ctxt format type_enc lambda_trans
-      |> map repair
+      repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
+                       |> map repair
     val poly_nonmono_Ts =
       if null nonmono_Ts orelse nonmono_Ts = [@{typ bool}] orelse
          polymorphism_of_type_enc type_enc <> Polymorphic then
--- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -23,6 +23,12 @@
     -> typ
   val is_type_surely_finite : Proof.context -> bool -> typ -> bool
   val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
+  val s_not : term -> term
+  val s_conj : term * term -> term
+  val s_disj : term * term -> term
+  val s_imp : term * term -> term
+  val s_iff : term * term -> term
+  val close_form : term -> term
   val monomorphic_term : Type.tyenv -> term -> term
   val eta_expand : typ list -> term -> int -> term
   val transform_elim_prop : term -> term
@@ -203,6 +209,39 @@
 fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
 fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
 
+(* Simple simplifications to ensure that sort annotations don't leave a trail of
+   spurious "True"s. *)
+fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
+    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
+  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
+    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
+  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
+  | s_not (@{const HOL.conj} $ t1 $ t2) =
+    @{const HOL.disj} $ s_not t1 $ s_not t2
+  | s_not (@{const HOL.disj} $ t1 $ t2) =
+    @{const HOL.conj} $ s_not t1 $ s_not t2
+  | s_not (@{const False}) = @{const True}
+  | s_not (@{const True}) = @{const False}
+  | s_not (@{const Not} $ t) = t
+  | s_not t = @{const Not} $ t
+fun s_conj (@{const True}, t2) = t2
+  | s_conj (t1, @{const True}) = t1
+  | s_conj p = HOLogic.mk_conj p
+fun s_disj (@{const False}, t2) = t2
+  | s_disj (t1, @{const False}) = t1
+  | s_disj p = HOLogic.mk_disj p
+fun s_imp (@{const True}, t2) = t2
+  | s_imp (t1, @{const False}) = s_not t1
+  | s_imp p = HOLogic.mk_imp p
+fun s_iff (@{const True}, t2) = t2
+  | s_iff (t1, @{const True}) = t1
+  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
+
+fun close_form t =
+  fold (fn ((x, i), T) => fn t' =>
+           HOLogic.all_const T $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
+       (Term.add_vars t []) t
+
 fun monomorphic_term subst =
   map_types (map_type_tvar (fn v =>
       case Type.lookup subst v of
--- a/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -197,7 +197,8 @@
     *)
     val (atp_problem, _, _, _, _, _, sym_tab) =
       prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
-                          combinatorsN false false [] @{prop False} props
+                          (rpair [] o map (introduce_combinators ctxt))
+                          false false [] @{prop False} props
     (*
     val _ = tracing ("ATP PROBLEM: " ^
                      cat_lines (tptp_lines_for_atp_problem CNF atp_problem))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -60,6 +60,11 @@
   type prover =
     params -> (string -> minimize_command) -> prover_problem -> prover_result
 
+  val concealedN : string
+  val liftingN : string
+  val combinatorsN : string
+  val lambdasN : string
+  val smartN : string
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
   val measure_run_time : bool Config.T
@@ -329,6 +334,12 @@
 
 (* configuration attributes *)
 
+val concealedN = "concealed"
+val liftingN = "lifting"
+val combinatorsN = "combinators"
+val lambdasN = "lambdas"
+val smartN = "smart"
+
 (* Empty string means create files in Isabelle's temporary files directory. *)
 val dest_dir =
   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
@@ -514,17 +525,29 @@
    | NONE => type_enc_from_string best_type_enc)
   |> choose_format formats
 
-fun effective_atp_lambda_translation ctxt type_enc =
+fun translate_atp_lambdas ctxt type_enc =
   Config.get ctxt atp_lambda_translation
   |> (fn trans =>
          if trans = smartN then
            if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
          else if trans = lambdasN andalso
                  not (is_type_enc_higher_order type_enc) then
-           error ("Lambda translation method incompatible with \
-                  \first-order encoding.")
+           error ("Lambda translation method incompatible with first-order \
+                  \encoding.")
          else
            trans)
+  |> (fn trans =>
+         if trans = concealedN then
+           rpair [] o map (conceal_lambdas ctxt)
+         else if trans = liftingN then
+           map (close_form o Envir.eta_contract)
+           #> SMT_Translate.lift_lambdas ctxt false #> snd #> swap
+         else if trans = combinatorsN then
+           rpair [] o map (introduce_combinators ctxt)
+         else if trans = lambdasN then
+           rpair [] o map (Envir.eta_contract)
+         else
+           error ("Unknown lambda translation method: " ^ quote trans ^ "."))
 
 val metis_minimize_max_time = seconds 2.0
 
@@ -657,8 +680,7 @@
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_enc sound false
-                      (effective_atp_lambda_translation ctxt type_enc)
+                      type_enc sound false (translate_atp_lambdas ctxt type_enc)
                       (Config.get ctxt atp_readable_names) true hyp_ts concl_t
                       facts
                 fun weights () = atp_problem_weights atp_problem
--- a/src/HOL/Tools/refute.ML	Sun Jul 17 20:23:33 2011 +0200
+++ b/src/HOL/Tools/refute.ML	Sun Jul 17 20:23:39 2011 +0200
@@ -62,7 +62,6 @@
 (* Additional functions used by Nitpick (to be factored out)                 *)
 (* ------------------------------------------------------------------------- *)
 
-  val close_form : term -> term
   val get_classdef : theory -> string -> (string * term) option
   val norm_rhs : term -> term
   val get_def : theory -> string * typ -> (string * term) option