diff -r 7e227e9de779 -r f132d13fcf75 src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu May 12 15:29:19 2011 +0200 @@ -355,24 +355,11 @@ subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j)) (0 upto length Ts - 1 ~~ Ts)) -(* Removes the lambdas from an equation of the form "t = (%x. u)". - (Cf. "extensionalize_theorem" in "Meson_Clausify".) *) -fun extensionalize_term t = - let - fun aux j (@{const Trueprop} \$ t') = @{const Trueprop} \$ aux j t' - | aux j (t as Const (s, Type (_, [Type (_, [_, T']), - Type (_, [_, res_T])])) - \$ t2 \$ Abs (var_s, var_T, t')) = - if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then - let val var_t = Var ((var_s, j), var_T) in - Const (s, T' --> T' --> res_T) - \$ betapply (t2, var_t) \$ subst_bound (var_t, t') - |> aux (j + 1) - end - else - t - | aux _ t = t - in aux (maxidx_of_term t + 1) t end +fun extensionalize_term ctxt t = + let val thy = Proof_Context.theory_of ctxt in + t |> cterm_of thy |> Meson.extensionalize_conv ctxt + |> prop_of |> Logic.dest_equals |> snd + end fun introduce_combinators_in_term ctxt kind t = let val thy = Proof_Context.theory_of ctxt in @@ -436,7 +423,7 @@ val t = t |> need_trueprop ? HOLogic.mk_Trueprop |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) [] - |> extensionalize_term + |> extensionalize_term ctxt |> presimp ? presimplify_term thy |> perhaps (try (HOLogic.dest_Trueprop)) |> introduce_combinators_in_term ctxt kind