diff -r 9070a7c356c9 -r 43c934dd4bc3 src/HOL/ex/svc_funcs.ML
--- a/src/HOL/ex/svc_funcs.ML	Mon Aug 30 09:28:02 2010 +0200
+++ b/src/HOL/ex/svc_funcs.ML	Mon Aug 30 09:35:30 2010 +0200
@@ -95,7 +95,7 @@
            | 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
@@ -200,7 +200,7 @@
             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])