1.1 --- a/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:11:35 2011 +0200
     1.2 +++ b/src/HOL/TPTP/atp_export.ML	Sun Jul 17 14:12:45 2011 +0200
     1.3 @@ -160,8 +160,8 @@
     1.4        facts
     1.5        |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
     1.6        |> prepare_atp_problem ctxt format Axiom Axiom type_enc true true
     1.7 -                             (map (introduce_combinators ctxt o snd)) false true
     1.8 -                             [] @{prop False}
     1.9 +                             (rpair [] o map (introduce_combinators ctxt))
    1.10 +                             false true [] @{prop False}
    1.11      val atp_problem =
    1.12        atp_problem
    1.13        |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))

     2.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Sun Jul 17 14:11:35 2011 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Sun Jul 17 14:12:45 2011 +0200
     2.3 @@ -251,34 +251,6 @@
     2.4  
     2.5  (** Hard-core proof reconstruction: structured Isar proofs **)
     2.6  
     2.7 -(* Simple simplifications to ensure that sort annotations don't leave a trail of
     2.8 -   spurious "True"s. *)
     2.9 -fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    2.10 -    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
    2.11 -  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    2.12 -    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
    2.13 -  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
    2.14 -  | s_not (@{const HOL.conj} $ t1 $ t2) =
    2.15 -    @{const HOL.disj} $ s_not t1 $ s_not t2
    2.16 -  | s_not (@{const HOL.disj} $ t1 $ t2) =
    2.17 -    @{const HOL.conj} $ s_not t1 $ s_not t2
    2.18 -  | s_not (@{const False}) = @{const True}
    2.19 -  | s_not (@{const True}) = @{const False}
    2.20 -  | s_not (@{const Not} $ t) = t
    2.21 -  | s_not t = @{const Not} $ t
    2.22 -fun s_conj (@{const True}, t2) = t2
    2.23 -  | s_conj (t1, @{const True}) = t1
    2.24 -  | s_conj p = HOLogic.mk_conj p
    2.25 -fun s_disj (@{const False}, t2) = t2
    2.26 -  | s_disj (t1, @{const False}) = t1
    2.27 -  | s_disj p = HOLogic.mk_disj p
    2.28 -fun s_imp (@{const True}, t2) = t2
    2.29 -  | s_imp (t1, @{const False}) = s_not t1
    2.30 -  | s_imp p = HOLogic.mk_imp p
    2.31 -fun s_iff (@{const True}, t2) = t2
    2.32 -  | s_iff (t1, @{const True}) = t1
    2.33 -  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    2.34 -
    2.35  fun forall_of v t = HOLogic.all_const (fastype_of v) $ lambda v t
    2.36  fun exists_of v t = HOLogic.exists_const (fastype_of v) $ lambda v t
    2.37  

     3.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     3.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Sun Jul 17 14:12:45 2011 +0200
     3.3 @@ -3,7 +3,7 @@
     3.4      Author:     Makarius
     3.5      Author:     Jasmin Blanchette, TU Muenchen
     3.6  
     3.7 -Translation of HOL to FOL for Sledgehammer.
     3.8 +Translation of HOL to FOL for Metis and Sledgehammer.
     3.9  *)
    3.10  
    3.11  signature ATP_TRANSLATE =
    3.12 @@ -92,8 +92,8 @@
    3.13    val introduce_combinators : Proof.context -> term -> term
    3.14    val prepare_atp_problem :
    3.15      Proof.context -> format -> formula_kind -> formula_kind -> type_enc -> bool
    3.16 -    -> bool -> ((formula_kind * term) list -> term list) -> bool -> bool
    3.17 -    -> term list -> term -> ((string * locality) * term) list
    3.18 +    -> bool -> (term list -> term list * term list) -> bool -> bool -> term list
    3.19 +    -> term -> ((string * locality) * term) list
    3.20      -> string problem * string Symtab.table * int * int
    3.21         * (string * locality) list vector * int list * int Symtab.table
    3.22    val atp_problem_weights : string problem -> (string * real) list
    3.23 @@ -120,15 +120,13 @@
    3.24  val bound_var_prefix = "B_"
    3.25  val schematic_var_prefix = "V_"
    3.26  val fixed_var_prefix = "v_"
    3.27 -
    3.28  val tvar_prefix = "T_"
    3.29  val tfree_prefix = "t_"
    3.30 -
    3.31  val const_prefix = "c_"
    3.32  val type_const_prefix = "tc_"
    3.33  val class_prefix = "cl_"
    3.34  
    3.35 -val skolem_const_prefix = "Sledgehammer" ^ Long_Name.separator ^ "Sko"
    3.36 +val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
    3.37  val old_skolem_const_prefix = skolem_const_prefix ^ "o"
    3.38  val new_skolem_const_prefix = skolem_const_prefix ^ "n"
    3.39  
    3.40 @@ -143,6 +141,7 @@
    3.41  val arity_clause_prefix = "arity_"
    3.42  val tfree_clause_prefix = "tfree_"
    3.43  
    3.44 +val lambda_fact_prefix = "ATP.lambda_"
    3.45  val typed_helper_suffix = "_T"
    3.46  val untyped_helper_suffix = "_U"
    3.47  val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
    3.48 @@ -158,9 +157,9 @@
    3.49  val prefixed_type_tag_name = const_prefix ^ type_tag_name
    3.50  
    3.51  (* Freshness almost guaranteed! *)
    3.52 -val sledgehammer_weak_prefix = "Sledgehammer:"
    3.53 +val atp_weak_prefix = "ATP:"
    3.54  
    3.55 -val concealed_lambda_prefix = sledgehammer_weak_prefix ^ "lambda_"
    3.56 +val concealed_lambda_prefix = atp_weak_prefix ^ "lambda_"
    3.57  
    3.58  (*Escaping of special characters.
    3.59    Alphanumeric characters are left unchanged.
    3.60 @@ -879,7 +878,7 @@
    3.61              #> Meson.presimplify ctxt
    3.62              #> prop_of)
    3.63  
    3.64 -fun concealed_bound_name j = sledgehammer_weak_prefix ^ string_of_int j
    3.65 +fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
    3.66  fun conceal_bounds Ts t =
    3.67    subst_bounds (map (Free o apfst concealed_bound_name)
    3.68                      (0 upto length Ts - 1 ~~ Ts), t)
    3.69 @@ -901,29 +900,34 @@
    3.70      t
    3.71  
    3.72  fun simple_translate_lambdas do_lambdas ctxt t =
    3.73 -  let
    3.74 -    fun aux Ts t =
    3.75 -      case t of
    3.76 -        @{const Not} $ t1 => @{const Not} $ aux Ts t1
    3.77 -      | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
    3.78 -        t0 $ Abs (s, T, aux (T :: Ts) t')
    3.79 -      | (t0 as Const (@{const_name All}, _)) $ t1 =>
    3.80 -        aux Ts (t0 $ eta_expand Ts t1 1)
    3.81 -      | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
    3.82 -        t0 $ Abs (s, T, aux (T :: Ts) t')
    3.83 -      | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
    3.84 -        aux Ts (t0 $ eta_expand Ts t1 1)
    3.85 -      | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    3.86 -      | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    3.87 -      | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
    3.88 -      | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
    3.89 -          $ t1 $ t2 =>
    3.90 -        t0 $ aux Ts t1 $ aux Ts t2
    3.91 -      | _ =>
    3.92 -        if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
    3.93 -        else t |> Envir.eta_contract |> do_lambdas ctxt Ts
    3.94 -    val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
    3.95 -  in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
    3.96 +  let val thy = Proof_Context.theory_of ctxt in
    3.97 +    if Meson.is_fol_term thy t then
    3.98 +      t
    3.99 +    else
   3.100 +      let
   3.101 +        fun aux Ts t =
   3.102 +          case t of
   3.103 +            @{const Not} $ t1 => @{const Not} $ aux Ts t1
   3.104 +          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   3.105 +            t0 $ Abs (s, T, aux (T :: Ts) t')
   3.106 +          | (t0 as Const (@{const_name All}, _)) $ t1 =>
   3.107 +            aux Ts (t0 $ eta_expand Ts t1 1)
   3.108 +          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   3.109 +            t0 $ Abs (s, T, aux (T :: Ts) t')
   3.110 +          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   3.111 +            aux Ts (t0 $ eta_expand Ts t1 1)
   3.112 +          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.113 +          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.114 +          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   3.115 +          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   3.116 +              $ t1 $ t2 =>
   3.117 +            t0 $ aux Ts t1 $ aux Ts t2
   3.118 +          | _ =>
   3.119 +            if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
   3.120 +            else t |> Envir.eta_contract |> do_lambdas ctxt Ts
   3.121 +        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   3.122 +      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   3.123 +  end
   3.124  
   3.125  fun do_conceal_lambdas Ts (t1 $ t2) =
   3.126      do_conceal_lambdas Ts t1 $ do_conceal_lambdas Ts t2
   3.127 @@ -946,11 +950,16 @@
   3.128    handle THM _ => do_conceal_lambdas Ts t
   3.129  val introduce_combinators = simple_translate_lambdas do_introduce_combinators
   3.130  
   3.131 -fun process_abstractions_in_terms ctxt trans_lambdas ps =
   3.132 +fun preprocess_abstractions_in_terms ctxt trans_lambdas facts =
   3.133    let
   3.134 -    val thy = Proof_Context.theory_of ctxt
   3.135 -    val (fo_ps, ho_ps) = ps |> List.partition (Meson.is_fol_term thy o snd)
   3.136 -  in map snd fo_ps @ trans_lambdas ho_ps end
   3.137 +    val (facts, lambda_ts) =
   3.138 +      facts |> map (snd o snd) |> trans_lambdas 
   3.139 +            |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
   3.140 +    val lambda_facts =
   3.141 +      map2 (fn t => fn j =>
   3.142 +               ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
   3.143 +           lambda_ts (1 upto length lambda_ts)
   3.144 +  in (facts, lambda_facts) end
   3.145  
   3.146  (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   3.147     same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
   3.148 @@ -959,11 +968,11 @@
   3.149      fun aux (t $ u) = aux t $ aux u
   3.150        | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   3.151        | aux (Var ((s, i), T)) =
   3.152 -        Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   3.153 +        Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   3.154        | aux t = t
   3.155    in t |> exists_subterm is_Var t ? aux end
   3.156  
   3.157 -fun preprocess_prop ctxt presimp_consts t =
   3.158 +fun presimp_prop ctxt presimp_consts t =
   3.159    let
   3.160      val thy = Proof_Context.theory_of ctxt
   3.161      val t = t |> Envir.beta_eta_contract
   3.162 @@ -1002,9 +1011,8 @@
   3.163      val thy = Proof_Context.theory_of ctxt
   3.164      val last = length ps - 1
   3.165    in
   3.166 -    map2 (fn j => fn (kind, t) =>
   3.167 -             t |> make_formula thy type_enc (format <> CNF) (string_of_int j)
   3.168 -                               Local kind
   3.169 +    map2 (fn j => fn ((name, loc), (kind, t)) =>
   3.170 +             t |> make_formula thy type_enc (format <> CNF) name loc kind
   3.171                 |> (j <> last) = (kind = Conjecture) ? update_iformula mk_anot)
   3.172           (0 upto last) ps
   3.173    end
   3.174 @@ -1426,29 +1434,32 @@
   3.175    let
   3.176      val thy = Proof_Context.theory_of ctxt
   3.177      val presimp_consts = Meson.presimplified_consts ctxt
   3.178 -    fun preprocess kind =
   3.179 -      preprocess_prop ctxt presimp_consts
   3.180 -      #> pair kind #> single
   3.181 -      #> process_abstractions_in_terms ctxt trans_lambdas
   3.182 -      #> the_single
   3.183      val fact_ts = facts |> map snd
   3.184      (* Remove existing facts from the conjecture, as this can dramatically
   3.185         boost an ATP's performance (for some reason). *)
   3.186      val hyp_ts =
   3.187        hyp_ts
   3.188        |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
   3.189 -    val fact_ts = facts |> map snd |> preproc ? map (preprocess Axiom)
   3.190 +    val fact_ps = facts |> map (apsnd (pair Axiom))
   3.191      val conj_ps =
   3.192        map (pair prem_kind) hyp_ts @ [(Conjecture, concl_t)]
   3.193 -      |> preproc
   3.194 -         ? map (fn (kind, t) => (kind, t |> preprocess kind |> freeze_term))
   3.195 -    val (facts, fact_names) =
   3.196 -      map2 (fn (name, _) => fn t =>
   3.197 -               (make_fact ctxt format type_enc true (name, t), name))
   3.198 -           facts fact_ts
   3.199 -      |> map_filter (try (apfst the))
   3.200 +      |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
   3.201 +    val ((conj_ps, fact_ps), lambda_ps) =
   3.202 +      conj_ps @ fact_ps
   3.203 +      |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
   3.204 +      |> (if preproc then preprocess_abstractions_in_terms ctxt trans_lambdas
   3.205 +          else rpair [])
   3.206 +      |>> chop (length conj_ps)
   3.207 +      |>> preproc ? apfst (map (apsnd (apsnd freeze_term)))
   3.208 +    val conjs = make_conjecture ctxt format type_enc conj_ps
   3.209 +    val (fact_names, facts) =
   3.210 +      fact_ps
   3.211 +      |> map_filter (fn (name, (_, t)) =>
   3.212 +                        make_fact ctxt format type_enc true (name, t)
   3.213 +                        |> Option.map (pair name))
   3.214        |> ListPair.unzip
   3.215 -    val conjs = make_conjecture ctxt format type_enc conj_ps
   3.216 +    val lambdas =
   3.217 +      lambda_ps |> map_filter (make_fact ctxt format type_enc false o apsnd snd)
   3.218      val all_ts = concl_t :: hyp_ts @ fact_ts
   3.219      val subs = tfree_classes_of_terms all_ts
   3.220      val supers = tvar_classes_of_terms all_ts
   3.221 @@ -1458,7 +1469,8 @@
   3.222        else make_arity_clauses thy tycons supers
   3.223      val class_rel_clauses = make_class_rel_clauses thy subs supers
   3.224    in
   3.225 -    (fact_names |> map single, (conjs, facts, class_rel_clauses, arity_clauses))
   3.226 +    (fact_names |> map single,
   3.227 +     (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
   3.228    end
   3.229  
   3.230  fun fo_literal_from_type_literal (TyLitVar (class, name)) =

     4.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:11:35 2011 +0200
     4.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Sun Jul 17 14:12:45 2011 +0200
     4.3 @@ -23,6 +23,11 @@
     4.4      -> typ
     4.5    val is_type_surely_finite : Proof.context -> bool -> typ -> bool
     4.6    val is_type_surely_infinite : Proof.context -> bool -> typ -> bool
     4.7 +  val s_not : term -> term
     4.8 +  val s_conj : term * term -> term
     4.9 +  val s_disj : term * term -> term
    4.10 +  val s_imp : term * term -> term
    4.11 +  val s_iff : term * term -> term
    4.12    val monomorphic_term : Type.tyenv -> term -> term
    4.13    val eta_expand : typ list -> term -> int -> term
    4.14    val transform_elim_prop : term -> term
    4.15 @@ -203,6 +208,34 @@
    4.16  fun is_type_surely_finite ctxt sound T = tiny_card_of_type ctxt sound 0 T <> 0
    4.17  fun is_type_surely_infinite ctxt sound T = tiny_card_of_type ctxt sound 1 T = 0
    4.18  
    4.19 +(* Simple simplifications to ensure that sort annotations don't leave a trail of
    4.20 +   spurious "True"s. *)
    4.21 +fun s_not (Const (@{const_name All}, T) $ Abs (s, T', t')) =
    4.22 +    Const (@{const_name Ex}, T) $ Abs (s, T', s_not t')
    4.23 +  | s_not (Const (@{const_name Ex}, T) $ Abs (s, T', t')) =
    4.24 +    Const (@{const_name All}, T) $ Abs (s, T', s_not t')
    4.25 +  | s_not (@{const HOL.implies} $ t1 $ t2) = @{const HOL.conj} $ t1 $ s_not t2
    4.26 +  | s_not (@{const HOL.conj} $ t1 $ t2) =
    4.27 +    @{const HOL.disj} $ s_not t1 $ s_not t2
    4.28 +  | s_not (@{const HOL.disj} $ t1 $ t2) =
    4.29 +    @{const HOL.conj} $ s_not t1 $ s_not t2
    4.30 +  | s_not (@{const False}) = @{const True}
    4.31 +  | s_not (@{const True}) = @{const False}
    4.32 +  | s_not (@{const Not} $ t) = t
    4.33 +  | s_not t = @{const Not} $ t
    4.34 +fun s_conj (@{const True}, t2) = t2
    4.35 +  | s_conj (t1, @{const True}) = t1
    4.36 +  | s_conj p = HOLogic.mk_conj p
    4.37 +fun s_disj (@{const False}, t2) = t2
    4.38 +  | s_disj (t1, @{const False}) = t1
    4.39 +  | s_disj p = HOLogic.mk_disj p
    4.40 +fun s_imp (@{const True}, t2) = t2
    4.41 +  | s_imp (t1, @{const False}) = s_not t1
    4.42 +  | s_imp p = HOLogic.mk_imp p
    4.43 +fun s_iff (@{const True}, t2) = t2
    4.44 +  | s_iff (t1, @{const True}) = t1
    4.45 +  | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
    4.46 +
    4.47  fun monomorphic_term subst =
    4.48    map_types (map_type_tvar (fn v =>
    4.49        case Type.lookup subst v of

     5.1 --- a/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 14:11:35 2011 +0200
     5.2 +++ b/src/HOL/Tools/Metis/metis_translate.ML	Sun Jul 17 14:12:45 2011 +0200
     5.3 @@ -197,8 +197,8 @@
     5.4      *)
     5.5      val (atp_problem, _, _, _, _, _, sym_tab) =
     5.6        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc true false
     5.7 -                          (map (introduce_combinators ctxt o snd)) false false
     5.8 -                          [] @{prop False} props
     5.9 +                          (rpair [] o map (introduce_combinators ctxt))
    5.10 +                          false false [] @{prop False} props
    5.11      (*
    5.12      val _ = tracing ("ATP PROBLEM: " ^
    5.13                       cat_lines (tptp_lines_for_atp_problem CNF atp_problem))

     6.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:11:35 2011 +0200
     6.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Jul 17 14:12:45 2011 +0200
     6.3 @@ -60,8 +60,8 @@
     6.4    type prover =
     6.5      params -> (string -> minimize_command) -> prover_problem -> prover_result
     6.6  
     6.7 -  val concealed_lambdasN : string
     6.8 -  val lambda_liftingN : string
     6.9 +  val concealedN : string
    6.10 +  val liftingN : string
    6.11    val combinatorsN : string
    6.12    val lambdasN : string
    6.13    val smartN : string
    6.14 @@ -334,8 +334,8 @@
    6.15  
    6.16  (* configuration attributes *)
    6.17  
    6.18 -val concealed_lambdasN = "concealed_lambdas"
    6.19 -val lambda_liftingN = "lambda_lifting"
    6.20 +val concealedN = "concealed"
    6.21 +val liftingN = "lifting"
    6.22  val combinatorsN = "combinators"
    6.23  val lambdasN = "lambdas"
    6.24  val smartN = "smart"
    6.25 @@ -525,15 +525,6 @@
    6.26     | NONE => type_enc_from_string best_type_enc)
    6.27    |> choose_format formats
    6.28  
    6.29 -fun lift_lambdas ctxt ps =
    6.30 -  let
    6.31 -    val ts = map snd ps (*###*)
    6.32 -  in
    6.33 -    case SMT_Translate.lift_lambdas ctxt false ts |> snd of
    6.34 -      (defs, [t]) => [foldr1 HOLogic.mk_conj (t :: defs)] (* FIXME: hack *)
    6.35 -    | (defs, ts) => ts @ defs
    6.36 -  end
    6.37 -
    6.38  fun translate_atp_lambdas ctxt type_enc =
    6.39    Config.get ctxt atp_lambda_translation
    6.40    |> (fn trans =>
    6.41 @@ -546,14 +537,14 @@
    6.42           else
    6.43             trans)
    6.44    |> (fn trans =>
    6.45 -         if trans = concealed_lambdasN then
    6.46 -           map (conceal_lambdas ctxt o snd)
    6.47 -         else if trans = lambda_liftingN then
    6.48 -           lift_lambdas ctxt
    6.49 +         if trans = concealedN then
    6.50 +           rpair [] o map (conceal_lambdas ctxt)
    6.51 +         else if trans = liftingN then
    6.52 +           SMT_Translate.lift_lambdas ctxt false #> snd #> swap
    6.53           else if trans = combinatorsN then
    6.54 -           map (introduce_combinators ctxt o snd)
    6.55 +           rpair [] o map (introduce_combinators ctxt)
    6.56           else if trans = lambdasN then
    6.57 -           map (Envir.eta_contract o snd)
    6.58 +           rpair [] o map (Envir.eta_contract)
    6.59           else
    6.60             error ("Unknown lambda translation method: " ^ quote trans ^ "."))
    6.61