src/HOL/Tools/Nitpick/nitpick_preproc.ML

 val may_use_binary_ints =
   let
     fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
       | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2
-      | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) =
+      | aux def (Const (@{const_name HOL.eq}, _) $ t1 $ t2) =
         aux def t1 andalso aux false t2
       | aux def (@{const HOL.implies} $ t1 $ t2) = aux false t1 andalso aux def t2
       | aux def (t1 $ t2) = aux def t1 andalso aux def t2
       | aux def (t as Const (s, _)) =
         (not def orelse t <> @{const Suc}) andalso

       | _ => exists_subterm (curry (op =) (Var z)) t' ? insert (op =) T
     fun box_var_in_def new_Ts old_Ts t (z as (_, T)) =
       case t of
         @{const Trueprop} $ t1 => box_var_in_def new_Ts old_Ts t1 z
       | Const (s0, _) $ t1 $ _ =>
-        if s0 = @{const_name "=="} orelse s0 = @{const_name "op ="} then
+        if s0 = @{const_name "=="} orelse s0 = @{const_name HOL.eq} then
           let
             val (t', args) = strip_comb t1
             val T' = fastype_of1 (new_Ts, do_term new_Ts old_Ts Neut t')
           in
             case fold (add_boxed_types_for_var z)

         @{const Not} $ do_term new_Ts old_Ts (flip_polarity polar) t1
       | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
       | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
         do_quantifier new_Ts old_Ts polar s0 T0 s1 T1 t1
-      | Const (s0 as @{const_name "op ="}, T0) $ t1 $ t2 =>
+      | Const (s0 as @{const_name HOL.eq}, T0) $ t1 $ t2 =>
         do_equals new_Ts old_Ts s0 T0 t1 t2
       | @{const HOL.conj} $ t1 $ t2 =>
         @{const HOL.conj} $ do_term new_Ts old_Ts polar t1
         $ do_term new_Ts old_Ts polar t2
       | @{const HOL.disj} $ t1 $ t2 =>

       case t of
         (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
       | (t0 as @{const "==>"}) $ t1 $ t2 =>
         if def then (t, []) else do_eq_or_imp Ts false def t0 t1 t2 seen
-      | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
+      | (t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2 =>
         do_eq_or_imp Ts true def t0 t1 t2 seen
       | (t0 as @{const HOL.implies}) $ t1 $ t2 =>
         do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in

                     | _ => I) t (K 0)
     fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
         aux_eq careful true t0 t1 t2
       | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
-      | aux careful ((t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2) =
+      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
         aux_eq careful true t0 t1 t2
       | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
         t0 $ aux false t1 $ aux careful t2
       | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
       | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2

         @{const "==>"} $ t1 $ t2 => aux_implies prems zs t1 t2
       | _ => Logic.list_implies (rev prems, t)
     and aux_implies prems zs t1 t2 =
       case t1 of
         Const (@{const_name "=="}, _) $ Var z $ t' => aux_eq prems zs z t' t1 t2
-      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ Var z $ t') =>
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Var z $ t') =>
         aux_eq prems zs z t' t1 t2
-      | @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t' $ Var z) =>
+      | @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t' $ Var z) =>
         aux_eq prems zs z t' t1 t2
       | _ => aux (t1 :: prems) (Term.add_vars t1 zs) t2
     and aux_eq prems zs z t' t1 t2 =
       if not (member (op =) zs z) andalso
          not (exists_subterm (curry (op =) (Var z)) t') then

                  raise SAME ()
              | _ => raise SAME ())
             handle SAME () => do_term (t :: seen) ts
         in
           case t of
-            Const (@{const_name "op ="}, _) $ t1 $ t2 => do_eq true t1 t2
+            Const (@{const_name HOL.eq}, _) $ t1 $ t2 => do_eq true t1 t2
           | _ => do_term (t :: seen) ts
         end
   in do_term end
 
 fun subst_one_bound j arg t =

 
 (** Function specialization **)
 
 fun params_in_equation (@{const "==>"} $ _ $ t2) = params_in_equation t2
   | params_in_equation (@{const Trueprop} $ t1) = params_in_equation t1
-  | params_in_equation (Const (@{const_name "op ="}, _) $ t1 $ _) =
+  | params_in_equation (Const (@{const_name HOL.eq}, _) $ t1 $ _) =
     snd (strip_comb t1)
   | params_in_equation _ = []
 
 fun specialize_fun_axiom x x' fixed_js fixed_args extra_args t =
   let