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