src/HOL/Tools/Meson/meson.ML
 changeset 42760 d83802e7348e parent 42750 c8b1d9ee3758 child 42793 88bee9f6eec7
```     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
1.3 @@ -616,18 +616,14 @@
1.4      skolemize_with_choice_theorems ctxt (choice_theorems thy)
1.5    end
1.6
1.7 -fun is_Abs (Abs _) = true
1.8 -  | is_Abs _ = false
1.9 -
1.10 -(* Removes the lambdas from an equation of the form "t = (%x. u)".  *)
1.11 +(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
1.12 +   would be desirable to do this symmetrically but there's at least one existing
1.13 +   proof in "Tarski" that relies on the current behavior. *)
1.14  fun extensionalize_conv ctxt ct =
1.15    case term_of ct of
1.16 -    Const (@{const_name HOL.eq}, _) \$ t1 \$ t2 =>
1.17 -    ct |> (if is_Abs t1 orelse is_Abs t2 then
1.18 -             Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
1.19 -             then_conv extensionalize_conv ctxt
1.20 -           else
1.21 -             Conv.comb_conv (extensionalize_conv ctxt))
1.22 +    Const (@{const_name HOL.eq}, _) \$ _ \$ Abs _ =>
1.23 +    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
1.24 +           then_conv extensionalize_conv ctxt)
1.25    | _ \$ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
1.26    | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
1.27    | _ => Conv.all_conv ct
```