src/HOL/ex/svc_funcs.ML

             Buildin("=>", [fm (not pos) p, fm pos q])
       | fm pos (Const(@{const_name Not}, _) $ p) =
             Buildin("NOT", [fm (not pos) p])
       | fm pos (Const(@{const_name True}, _)) = TrueExpr
       | fm pos (Const(@{const_name False}, _)) = FalseExpr
-      | fm pos (Const("SVC_Oracle.iff_keep", _) $ p $ q) =
+      | fm pos (Const(@{const_name iff_keep}, _) $ p $ q) =
              (*polarity doesn't matter*)
             Buildin("=", [fm pos p, fm pos q])
-      | fm pos (Const("SVC_Oracle.iff_unfold", _) $ p $ q) =
+      | fm pos (Const(@{const_name 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 HOL.eq}, Type ("fun", [T,_])) $ x $ y) =
             let val tx = tm x and ty = tm y