1.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Mon Jan 30 17:15:59 2012 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Mon Jan 30 17:15:59 2012 +0100
     1.3 @@ -230,7 +230,8 @@
     1.4        fold_rev (fn (name, th) => fn (old_skolems, props) =>
     1.5                     th |> prop_of |> Logic.strip_imp_concl
     1.6                        |> conceal_old_skolem_terms (length clauses) old_skolems
     1.7 -                      ||> lam_trans = lam_liftingN ? eliminate_lam_wrappers
     1.8 +                      ||> (lam_trans = liftingN orelse lam_trans = lam_liftingN)
     1.9 +                          ? eliminate_lam_wrappers
    1.10                        ||> (fn prop => (name, prop) :: props))
    1.11                 clauses ([], [])
    1.12      (*
    1.13 @@ -238,7 +239,7 @@
    1.14        tracing ("PROPS:\n" ^
    1.15                 cat_lines (map (Syntax.string_of_term ctxt o snd) props))
    1.16      *)
    1.17 -    val lam_trans = if lam_trans = combinatorsN then no_lamsN else lam_trans
    1.18 +    val lam_trans = if lam_trans = combsN then no_lamsN else lam_trans
    1.19      val (atp_problem, _, _, lifted, sym_tab) =
    1.20        prepare_atp_problem ctxt CNF Hypothesis Axiom type_enc false lam_trans
    1.21                            false false [] @{prop False} props