src/HOL/Algebra/ringsimp.ML

 
 (*** 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.semigroup.mult"];
+  "CRing.minus", "Group.monoid.one", "Group.monoid.mult"];
 
 fun termless_ring (a, b) = (term_lpo ring_ord (a, b) = LESS);
 
 val cring_ss = HOL_ss settermless termless_ring;
 

     fun ring_filter t = (case HOLogic.dest_Trueprop t of
         Const ("CRing.ring_axioms", _) $ Free (s, _) => [s]
       | _ => [])
       handle TERM _ => [];
     fun comm_filter t = (case HOLogic.dest_Trueprop t of
-        Const ("Group.comm_semigroup_axioms", _) $ Free (s, _) => [s]
+        Const ("Group.comm_monoid_axioms", _) $ Free (s, _) => [s]
       | _ => [])
       handle TERM _ => [];
 
     val prems = ProofContext.prems_of ctxt;
     val rings = flat (map (ring_filter o #prop o rep_thm) prems);