1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -686,9 +686,11 @@
     1.4  
     1.5  (* Requires bound variables not to clash with any schematic variables (as should
     1.6     be the case right after lambda-lifting). *)
     1.7 -fun open_form (Const (@{const_name All}, _) $ Abs (_, T, t)) =
     1.8 -    subst_bound (Var ((Name.uu ^ Int.toString (size_of_term t), 0), T), t)
     1.9 -    |> open_form
    1.10 +fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) =
    1.11 +    let
    1.12 +      val names = Name.make_context (map fst (Term.add_var_names t []))
    1.13 +      val (s, _) = Name.variant s names
    1.14 +    in open_form (subst_bound (Var ((s, 0), T), t)) end
    1.15    | open_form t = t
    1.16  
    1.17  fun lift_lams_part_1 ctxt type_enc =

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 18 11:47:12 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Nov 18 11:47:12 2011 +0100
     2.3 @@ -267,9 +267,9 @@
     2.4    | s_iff (t1, t2) = HOLogic.eq_const HOLogic.boolT $ t1 $ t2
     2.5  
     2.6  fun close_form t =
     2.7 -  fold (fn ((x, i), T) => fn t' =>
     2.8 +  fold (fn ((s, i), T) => fn t' =>
     2.9             HOLogic.all_const T
    2.10 -           $ Abs (x, T, abstract_over (Var ((x, i), T), t')))
    2.11 +           $ Abs (s, T, abstract_over (Var ((s, i), T), t')))
    2.12         (Term.add_vars t []) t
    2.13  
    2.14  fun monomorphic_term subst =

     3.1 --- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     3.2 +++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
     3.3 @@ -67,22 +67,43 @@
     3.4      val ct = cterm_of thy (HOLogic.mk_Trueprop t)
     3.5    in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
     3.6  
     3.7 +fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
     3.8 +  | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
     3.9 +  | add_vars_and_frees (t as Var _) = insert (op =) t
    3.10 +  | add_vars_and_frees (t as Free _) = insert (op =) t
    3.11 +  | add_vars_and_frees _ = I
    3.12 +
    3.13  fun introduce_lam_wrappers ctxt th =
    3.14    if Meson_Clausify.is_quasi_lambda_free (prop_of th) then
    3.15      th
    3.16    else
    3.17      let
    3.18 -      fun conv wrap ctxt ct =
    3.19 +      val thy = Proof_Context.theory_of ctxt
    3.20 +      fun conv first ctxt ct =
    3.21          if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
    3.22            Thm.reflexive ct
    3.23          else case term_of ct of
    3.24 -          Abs _ =>
    3.25 -          Conv.abs_conv (conv false o snd) ctxt ct
    3.26 -          |> wrap
    3.27 -             ? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    3.28 +          t as Abs (_, _, u) =>
    3.29 +          if first then
    3.30 +            case add_vars_and_frees u [] of
    3.31 +              [] =>
    3.32 +              Conv.abs_conv (conv false o snd) ctxt ct
    3.33 +              |> (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI})
    3.34 +            | v :: _ =>
    3.35 +              Abs (Name.uu, fastype_of v, abstract_over (v, term_of ct)) $ v
    3.36 +              |> cterm_of thy
    3.37 +              |> Conv.comb_conv (conv true ctxt)
    3.38 +          else
    3.39 +            Conv.abs_conv (conv false o snd) ctxt ct
    3.40 +        | Const (@{const_name Meson.skolem}, _) $ _ => Thm.reflexive ct
    3.41          | _ => Conv.comb_conv (conv true ctxt) ct
    3.42 -      val eqth = conv true ctxt (cprop_of th)
    3.43 -    in Thm.equal_elim eqth th end
    3.44 +      val eq_th = conv true ctxt (cprop_of th)
    3.45 +      (* We replace the equation's left-hand side with a beta-equivalent term
    3.46 +         so that "Thm.equal_elim" works below. *)
    3.47 +      val t0 $ _ $ t2 = prop_of eq_th
    3.48 +      val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
    3.49 +      val eq_th' = Goal.prove_internal [] eq_ct (K (Tactic.rtac eq_th 1))
    3.50 +    in Thm.equal_elim eq_th' th end
    3.51  
    3.52  val clause_params =
    3.53    {ordering = Metis_KnuthBendixOrder.default,
    3.54 @@ -104,19 +125,18 @@
    3.55    let val thy = Proof_Context.theory_of ctxt
    3.56        val new_skolemizer =
    3.57          Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
    3.58 -      val preproc =
    3.59 -        Drule.eta_contraction_rule
    3.60 -        #> lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    3.61 -      val cls = cls |> map preproc
    3.62 -      val ths0 = ths0 |> map preproc
    3.63 +      val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
    3.64        val th_cls_pairs =
    3.65          map2 (fn j => fn th =>
    3.66                  (Thm.get_name_hint th,
    3.67 -                 Meson_Clausify.cnf_axiom ctxt new_skolemizer
    3.68 -                                          (lam_trans = combinatorsN) j th))
    3.69 +                 th |> Drule.eta_contraction_rule
    3.70 +                    |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
    3.71 +                                                (lam_trans = combinatorsN) j
    3.72 +                    ||> map do_lams))
    3.73               (0 upto length ths0 - 1) ths0
    3.74        val ths = maps (snd o snd) th_cls_pairs
    3.75        val dischargers = map (fst o snd) th_cls_pairs
    3.76 +      val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)
    3.77        val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
    3.78        val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls
    3.79        val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc)