--- a/src/HOL/Algebra/ringsimp.ML Fri Jul 14 14:19:48 2006 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Fri Jul 14 14:37:15 2006 +0200
@@ -7,9 +7,10 @@
(*** Term order for commutative rings ***)
-fun ring_ord a =
- find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
- "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
+fun ring_ord (Const (a, _)) =
+ find_index_eq a ["CRing.ring.zero", "CRing.ring.add", "CRing.a_inv",
+ "CRing.minus", "Group.monoid.one", "Group.monoid.mult"]
+ | ring_ord _ = ~1;
fun termless_ring (a, b) = (Term.term_lpo ring_ord (a, b) = LESS);