src/HOL/Tools/record.ML
changeset 38864 4abe644fcea5
parent 38857 97775f3e8722
child 39134 917b4b6ba3d2
     1.1 --- a/src/HOL/Tools/record.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -1342,7 +1342,7 @@
     1.4  val eq_simproc =
     1.5    Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
     1.6      (fn thy => fn _ => fn t =>
     1.7 -      (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
     1.8 +      (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
     1.9          (case rec_id ~1 T of
    1.10            "" => NONE
    1.11          | name =>
    1.12 @@ -1405,12 +1405,12 @@
    1.13                  else raise TERM ("", [x]);
    1.14                val sel' = Const (sel, Tsel) $ Bound 0;
    1.15                val (l, r) = if lr then (sel', x') else (x', sel');
    1.16 -            in Const (@{const_name "op ="}, Teq) $ l $ r end
    1.17 +            in Const (@{const_name HOL.eq}, Teq) $ l $ r end
    1.18            else raise TERM ("", [Const (sel, Tsel)]);
    1.19  
    1.20 -        fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
    1.21 +        fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
    1.22                (true, Teq, (sel, Tsel), X)
    1.23 -          | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
    1.24 +          | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
    1.25                (false, Teq, (sel, Tsel), X)
    1.26            | dest_sel_eq _ = raise TERM ("", []);
    1.27        in
    1.28 @@ -1845,7 +1845,7 @@
    1.29      val eq =
    1.30        (HOLogic.mk_Trueprop o HOLogic.mk_eq)
    1.31          (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
    1.32 -         Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
    1.33 +         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
    1.34      fun tac eq_def =
    1.35        Class.intro_classes_tac []
    1.36        THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])