src/Pure/raw_simplifier.ML
changeset 56245 84fc7dfa3cd4
parent 55635 00e900057b38
child 56438 7f6b2634d853
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -599,7 +599,7 @@
     1.4    | is_full_cong_prems [] _ = false
     1.5    | is_full_cong_prems (p :: prems) varpairs =
     1.6        (case Logic.strip_assums_concl p of
     1.7 -        Const ("==", _) $ lhs $ rhs =>
     1.8 +        Const ("Pure.eq", _) $ lhs $ rhs =>
     1.9            let val (x, xs) = strip_comb lhs and (y, ys) = strip_comb rhs in
    1.10              is_Var x andalso forall is_Bound xs andalso
    1.11              not (has_duplicates (op =) xs) andalso xs = ys andalso
    1.12 @@ -981,7 +981,7 @@
    1.13        let
    1.14          fun is_simple ({thm, ...}: rrule) =
    1.15            (case Thm.prop_of thm of
    1.16 -            Const ("==", _) $ _ $ _ => true
    1.17 +            Const ("Pure.eq", _) $ _ $ _ => true
    1.18            | _ => false);
    1.19          fun sort [] (re1, re2) = re1 @ re2
    1.20            | sort (rr :: rrs) (re1, re2) =
    1.21 @@ -1099,7 +1099,7 @@
    1.22                  end
    1.23              | t $ _ =>
    1.24                (case t of
    1.25 -                Const ("==>", _) $ _  => impc t0 ctxt
    1.26 +                Const ("Pure.imp", _) $ _  => impc t0 ctxt
    1.27                | Abs _ =>
    1.28                    let val thm = Thm.beta_conversion false t0
    1.29                    in