# HG changeset patch
# User blanchet
# Date 1305206959 -7200
# Node ID d83802e7348e9bd39743724a094f93b2bdf7f162
# Parent  fdd15e889ad7717c0fe2d11a367a502efd244e72
another concession to backward compatibility

diff -r fdd15e889ad7 -r d83802e7348e src/HOL/Metis_Examples/HO_Reas.thy
--- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
@@ -28,10 +28,6 @@
 sledgehammer [expect = some] (inc_def)
 by (metis inc_def)
 
-lemma "(\<lambda>y. y + 1) = inc"
-sledgehammer [expect = some] (inc_def)
-by (metis inc_def)
-
 definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
 "add_swap = (\<lambda>x y. y + x)"
 
diff -r fdd15e889ad7 -r d83802e7348e src/HOL/Tools/Meson/meson.ML
--- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
@@ -616,18 +616,14 @@
     skolemize_with_choice_theorems ctxt (choice_theorems thy)
   end
 
-fun is_Abs (Abs _) = true
-  | is_Abs _ = false
-
-(* Removes the lambdas from an equation of the form "t = (%x. u)".  *)
+(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
+   would be desirable to do this symmetrically but there's at least one existing
+   proof in "Tarski" that relies on the current behavior. *)
 fun extensionalize_conv ctxt ct =
   case term_of ct of
-    Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
-    ct |> (if is_Abs t1 orelse is_Abs t2 then
-             Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
-             then_conv extensionalize_conv ctxt
-           else
-             Conv.comb_conv (extensionalize_conv ctxt))
+    Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
+    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
+           then_conv extensionalize_conv ctxt)
   | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
   | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
   | _ => Conv.all_conv ct