--- a/src/HOL/Tools/res_clause.ML Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Tools/res_clause.ML Fri Jul 20 14:28:25 2007 +0200
@@ -89,8 +89,8 @@
(*Provide readable names for the more common symbolic functions*)
val const_trans_table =
Symtab.make [("op =", "equal"),
- (@{const_name Orderings.less_eq}, "lessequals"),
- (@{const_name Orderings.less}, "less"),
+ (@{const_name HOL.less_eq}, "lessequals"),
+ (@{const_name HOL.less}, "less"),
("op &", "and"),
("op |", "or"),
(@{const_name HOL.plus}, "plus"),