--- a/src/HOL/ex/svc_funcs.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/ex/svc_funcs.ML Sat Aug 28 16:14:32 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])