--- a/src/HOL/ex/svc_funcs.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/ex/svc_funcs.ML Fri Jul 20 14:28:25 2007 +0200
@@ -112,8 +112,8 @@
b1 orelse b2)
end
else (*might be numeric equality*) (t, is_intnat T)
- | Const(@{const_name Orderings.less}, Type ("fun", [T,_])) => (t, is_intnat T)
- | Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name HOL.less}, Type ("fun", [T,_])) => (t, is_intnat T)
+ | Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) => (t, is_intnat T)
| _ => (t, false)
end
in #1 o tag end;
@@ -216,13 +216,13 @@
else fail t
end
(*inequalities: possible types are nat, int, real*)
- | fm pos (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.less}, Type ("fun", [T,_])) $ x $ y) =
if not pos orelse T = HOLogic.realT then
Buildin("<", [tm x, tm y])
else if is_intnat T then
Buildin("<=", [suc (tm x), tm y])
else fail t
- | fm pos (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ x $ y) =
+ | fm pos (t as Const(@{const_name HOL.less_eq}, Type ("fun", [T,_])) $ x $ y) =
if pos orelse T = HOLogic.realT then
Buildin("<=", [tm x, tm y])
else if is_intnat T then