diff -r 980d4194a212 -r b48ab741683b src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Groups.thy	Sat Feb 27 23:13:01 2010 +0100
@@ -1216,7 +1216,7 @@
         @{const_name Groups.uminus}, @{const_name Groups.minus}]
   | agrp_ord _ = ~1;
 
-fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
+fun termless_agrp (a, b) = (Term_Ord.term_lpo agrp_ord (a, b) = LESS);
 
 local
   val ac1 = mk_meta_eq @{thm add_assoc};