another concession to backward compatibility
authorblanchet
Thu May 12 15:29:19 2011 +0200 (2011-05-12)
changeset 42760d83802e7348e
parent 42759 fdd15e889ad7
child 42761 8ea9c6fa8b53
another concession to backward compatibility
src/HOL/Metis_Examples/HO_Reas.thy
src/HOL/Tools/Meson/meson.ML
     1.1 --- a/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/HO_Reas.thy	Thu May 12 15:29:19 2011 +0200
     1.3 @@ -28,10 +28,6 @@
     1.4  sledgehammer [expect = some] (inc_def)
     1.5  by (metis inc_def)
     1.6  
     1.7 -lemma "(\<lambda>y. y + 1) = inc"
     1.8 -sledgehammer [expect = some] (inc_def)
     1.9 -by (metis inc_def)
    1.10 -
    1.11  definition add_swap :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    1.12  "add_swap = (\<lambda>x y. y + x)"
    1.13  
     2.1 --- a/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/Meson/meson.ML	Thu May 12 15:29:19 2011 +0200
     2.3 @@ -616,18 +616,14 @@
     2.4      skolemize_with_choice_theorems ctxt (choice_theorems thy)
     2.5    end
     2.6  
     2.7 -fun is_Abs (Abs _) = true
     2.8 -  | is_Abs _ = false
     2.9 -
    2.10 -(* Removes the lambdas from an equation of the form "t = (%x. u)".  *)
    2.11 +(* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
    2.12 +   would be desirable to do this symmetrically but there's at least one existing
    2.13 +   proof in "Tarski" that relies on the current behavior. *)
    2.14  fun extensionalize_conv ctxt ct =
    2.15    case term_of ct of
    2.16 -    Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>
    2.17 -    ct |> (if is_Abs t1 orelse is_Abs t2 then
    2.18 -             Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
    2.19 -             then_conv extensionalize_conv ctxt
    2.20 -           else
    2.21 -             Conv.comb_conv (extensionalize_conv ctxt))
    2.22 +    Const (@{const_name HOL.eq}, _) $ _ $ Abs _ =>
    2.23 +    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
    2.24 +           then_conv extensionalize_conv ctxt)
    2.25    | _ $ _ => Conv.comb_conv (extensionalize_conv ctxt) ct
    2.26    | Abs _ => Conv.abs_conv (extensionalize_conv o snd) ctxt ct
    2.27    | _ => Conv.all_conv ct