src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42747 f132d13fcf75
parent 42742 369dfc819056
child 42750 c8b1d9ee3758
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -355,24 +355,11 @@
     1.4    subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
     1.5                      (0 upto length Ts - 1 ~~ Ts))
     1.6  
     1.7 -(* Removes the lambdas from an equation of the form "t = (%x. u)".
     1.8 -   (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
     1.9 -fun extensionalize_term t =
    1.10 -  let
    1.11 -    fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
    1.12 -      | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
    1.13 -                                        Type (_, [_, res_T])]))
    1.14 -                    $ t2 $ Abs (var_s, var_T, t')) =
    1.15 -        if s = @{const_name HOL.eq} orelse s = @{const_name "=="} then
    1.16 -          let val var_t = Var ((var_s, j), var_T) in
    1.17 -            Const (s, T' --> T' --> res_T)
    1.18 -              $ betapply (t2, var_t) $ subst_bound (var_t, t')
    1.19 -            |> aux (j + 1)
    1.20 -          end
    1.21 -        else
    1.22 -          t
    1.23 -      | aux _ t = t
    1.24 -  in aux (maxidx_of_term t + 1) t end
    1.25 +fun extensionalize_term ctxt t =
    1.26 +  let val thy = Proof_Context.theory_of ctxt in
    1.27 +    t |> cterm_of thy |> Meson.extensionalize_conv ctxt
    1.28 +      |> prop_of |> Logic.dest_equals |> snd
    1.29 +  end
    1.30  
    1.31  fun introduce_combinators_in_term ctxt kind t =
    1.32    let val thy = Proof_Context.theory_of ctxt in
    1.33 @@ -436,7 +423,7 @@
    1.34      val t = t |> need_trueprop ? HOLogic.mk_Trueprop
    1.35                |> Raw_Simplifier.rewrite_term thy
    1.36                       (Meson.unfold_set_const_simps ctxt) []
    1.37 -              |> extensionalize_term
    1.38 +              |> extensionalize_term ctxt
    1.39                |> presimp ? presimplify_term thy
    1.40                |> perhaps (try (HOLogic.dest_Trueprop))
    1.41                |> introduce_combinators_in_term ctxt kind