diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/ex/svc_funcs.ML
--- 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