src/HOL/Tools/record.ML

  Complexity: #components * #updates     #updates
 *)
 val eq_simproc =
   Simplifier.simproc_global @{theory HOL} "record_eq_simp" ["r = s"]
     (fn thy => fn _ => fn t =>
-      (case t of Const (@{const_name "op ="}, Type (_, [T, _])) $ _ $ _ =>
+      (case t of Const (@{const_name HOL.eq}, Type (_, [T, _])) $ _ $ _ =>
         (case rec_id ~1 T of
           "" => NONE
         | name =>
             (case get_equalities thy name of
               NONE => NONE

                 if not (loose_bvar1 (x, 0))
                 then Free ("x" ^ string_of_int i, range_type Tsel)
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
-            in Const (@{const_name "op ="}, Teq) $ l $ r end
+            in Const (@{const_name HOL.eq}, Teq) $ l $ r end
           else raise TERM ("", [Const (sel, Tsel)]);
 
-        fun dest_sel_eq (Const (@{const_name "op ="}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
+        fun dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ (Const (sel, Tsel) $ Bound 0) $ X) =
               (true, Teq, (sel, Tsel), X)
-          | dest_sel_eq (Const (@{const_name "op ="}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
+          | dest_sel_eq (Const (@{const_name HOL.eq}, Teq) $ X $ (Const (sel, Tsel) $ Bound 0)) =
               (false, Teq, (sel, Tsel), X)
           | dest_sel_eq _ = raise TERM ("", []);
       in
         (case t of
           Const (@{const_name Ex}, Tex) $ Abs (s, T, t) =>

 fun add_code ext_tyco vs extT ext simps inject thy =
   let
     val eq =
       (HOLogic.mk_Trueprop o HOLogic.mk_eq)
         (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
-         Const (@{const_name "op ="}, extT --> extT --> HOLogic.boolT));
+         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT));
     fun tac eq_def =
       Class.intro_classes_tac []
       THEN (Simplifier.rewrite_goals_tac [Simpdata.mk_eq eq_def])
       THEN ALLGOALS (rtac @{thm refl});
     fun mk_eq thy eq_def = Simplifier.rewrite_rule