changeset 35408 | b48ab741683b |
parent 35364 | b8c62d60195c |
child 35720 | 3fc79186a2f6 |
--- 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};