src/HOL/simpdata.ML
changeset 16999 307b2ec590ff
parent 16633 208ebc9311f2
child 17003 b902e11b3df1
     1.1 --- a/src/HOL/simpdata.ML	Tue Aug 02 13:13:18 2005 +0200
     1.2 +++ b/src/HOL/simpdata.ML	Tue Aug 02 16:50:55 2005 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4  fun lift_meta_eq_to_obj_eq i st =
     1.5    let
     1.6      val {sign, ...} = rep_thm st;
     1.7 -    fun count_imp (Const ("HOL.simp_implies", _) $ P $ Q) = 1 + count_imp Q
     1.8 +    fun count_imp (Const ("HOL.op =simp=>", _) $ P $ Q) = 1 + count_imp Q
     1.9        | count_imp _ = 0;
    1.10      val j = count_imp (Logic.strip_assums_concl (List.nth (prems_of st, i - 1)))
    1.11    in if j = 0 then meta_eq_to_obj_eq
    1.12 @@ -216,7 +216,7 @@
    1.13        let
    1.14          val Ps = map (fn k => Free ("P" ^ string_of_int k, propT)) (1 upto j);
    1.15          fun mk_simp_implies Q = foldr (fn (R, S) =>
    1.16 -          Const ("HOL.simp_implies", propT --> propT --> propT) $ R $ S) Q Ps
    1.17 +          Const ("HOL.op =simp=>", propT --> propT --> propT) $ R $ S) Q Ps
    1.18          val aT = TFree ("'a", HOLogic.typeS);
    1.19          val x = Free ("x", aT);
    1.20          val y = Free ("y", aT)