src/HOL/Tools/int_arith.ML

   make_simproc {lhss = lhss1, name = "one_to_of_int_one_simproc",
   proc = proc1, identifier = []};
 
 fun check (Const (@{const_name Groups.one}, @{typ int})) = false
   | check (Const (@{const_name Groups.one}, _)) = true
-  | check (Const (s, _)) = member (op =) [@{const_name "op ="},
+  | check (Const (s, _)) = member (op =) [@{const_name HOL.eq},
       @{const_name Groups.times}, @{const_name Groups.uminus},
       @{const_name Groups.minus}, @{const_name Groups.plus},
       @{const_name Groups.zero},
       @{const_name Orderings.less}, @{const_name Orderings.less_eq}] s
   | check (a $ b) = check a andalso check b