--- a/src/HOL/Tools/res_clause.ML	Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Tools/res_clause.ML	Wed Feb 10 14:12:04 2010 +0100
@@ -99,7 +99,7 @@
 (*Provide readable names for the more common symbolic functions*)
 val const_trans_table =
       Symtab.make [(@{const_name "op ="}, "equal"),
-                   (@{const_name Algebras.less_eq}, "lessequals"),
+                   (@{const_name Orderings.less_eq}, "lessequals"),
                    (@{const_name "op &"}, "and"),
                    (@{const_name "op |"}, "or"),
                    (@{const_name "op -->"}, "implies"),