--- a/src/HOL/Algebra/ringsimp.ML Tue Apr 29 12:36:49 2003 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Wed Apr 30 10:01:35 2003 +0200
@@ -56,8 +56,8 @@
(*** Term order for commutative rings ***)
fun ring_ord a =
- find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "Cring.ring.a_inv",
- "CRing.ring.minus", "Group.monoid.one", "Group.semigroup.mult"];
+ find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
+ "CRing.minus", "Group.monoid.one", "Group.semigroup.mult"];
fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);