src/HOL/Tools/Meson/meson.ML
changeset 56245 84fc7dfa3cd4
parent 55990 41c6b99c5fb7
child 58839 ccda99401bc8
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -105,7 +105,7 @@
     1.4      try (fn () =>
     1.5        let val thy = theory_of_thm thA
     1.6            val tmA = concl_of thA
     1.7 -          val Const("==>",_) $ tmB $ _ = prop_of thB
     1.8 +          val Const(@{const_name Pure.imp},_) $ tmB $ _ = prop_of thB
     1.9            val tenv =
    1.10              Pattern.first_order_match thy (tmB, tmA)
    1.11                                            (Vartab.empty, Vartab.empty) |> snd
    1.12 @@ -472,7 +472,7 @@
    1.13  
    1.14  (***** MESON PROOF PROCEDURE *****)
    1.15  
    1.16 -fun rhyps (Const("==>",_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
    1.17 +fun rhyps (Const(@{const_name Pure.imp},_) $ (Const(@{const_name Trueprop},_) $ A) $ phi,
    1.18             As) = rhyps(phi, A::As)
    1.19    | rhyps (_, As) = As;
    1.20