--- a/src/HOL/OrderedGroup.thy Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/OrderedGroup.thy Wed Dec 31 15:30:10 2008 +0100
@@ -1,7 +1,5 @@
(* Title: HOL/OrderedGroup.thy
- ID: $Id$
- Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, and Markus Wenzel,
- with contributions by Jeremy Avigad
+ Author: Gertrud Bauer, Steven Obua, Lawrence C Paulson, Markus Wenzel, Jeremy Avigad
*)
header {* Ordered Groups *}
@@ -1376,7 +1374,7 @@
@{const_name HOL.uminus}, @{const_name HOL.minus}]
| agrp_ord _ = ~1;
-fun termless_agrp (a, b) = (Term.term_lpo agrp_ord (a, b) = LESS);
+fun termless_agrp (a, b) = (TermOrd.term_lpo agrp_ord (a, b) = LESS);
local
val ac1 = mk_meta_eq @{thm add_assoc};