--- a/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Wed Feb 10 14:12:04 2010 +0100
@@ -95,8 +95,8 @@
| fm ((c as Const("True", _))) = c
| fm ((c as Const("False", _))) = c
| fm (t as Const("op =", Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name Algebras.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
- | fm (t as Const(@{const_name Algebras.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
+ | fm (t as Const(@{const_name Orderings.less_eq}, Type ("fun", [T,_])) $ _ $ _) = rel (T, t)
| fm t = replace t
(*entry point, and abstraction of a meta-formula*)
fun mt ((c as Const("Trueprop", _)) $ p) = c $ (fm p)