src/HOL/ex/svc_funcs.ML

            | Const(@{const_name HOL.disj}, _)   => apply c (map tag ts)
            | Const(@{const_name HOL.implies}, _) => apply c (map tag ts)
            | Const(@{const_name Not}, _)    => apply c (map tag ts)
            | Const(@{const_name True}, _)   => (c, false)
            | Const(@{const_name False}, _)  => (c, false)
-           | Const(@{const_name "op ="}, Type ("fun", [T,_])) =>
+           | Const(@{const_name HOL.eq}, Type ("fun", [T,_])) =>
                  if T = HOLogic.boolT then
                      (*biconditional: with int/nat comparisons below?*)
                      let val [t1,t2] = ts
                          val (u1,b1) = tag t1
                          and (u2,b2) = tag t2

             Buildin("=", [fm pos p, fm pos q])
       | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
             Buildin("AND",   (*unfolding uses both polarities*)
                          [Buildin("=>", [fm (not pos) p, fm pos q]),
                           Buildin("=>", [fm (not pos) q, fm pos p])])
-      | fm pos (t as Const(@{const_name "op ="}, Type ("fun", [T,_])) $ x $ y) =
+      | fm pos (t as Const(@{const_name HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
             let val tx = tm x and ty = tm y
                 in if pos orelse T = HOLogic.realT then
                        Buildin("=", [tx, ty])
                    else if is_intnat T then
                        Buildin("AND",