src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
 changeset 42747 f132d13fcf75 parent 42742 369dfc819056 child 42750 c8b1d9ee3758
```--- 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```