diff -r 92ed032e83a1 -r 0ae66ffb9784 src/HOL/Algebra/CRing.thy
--- a/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:27:50 2003 +0100
+++ b/src/HOL/Algebra/CRing.thy	Wed Dec 10 14:29:05 2003 +0100
@@ -90,7 +90,7 @@
   by (unfold comm_semigroup_def semigroup_def)
     (fast intro: comm_monoid.axioms a_comm_monoid)
 
-lemmas monoid_record_simps = semigroup.simps monoid.simps
+lemmas monoid_record_simps = partial_object.simps semigroup.simps monoid.simps
 
 lemma (in abelian_monoid) a_closed [intro, simp]:
   "[| x \<in> carrier G; y \<in> carrier G |] ==> x \<oplus> y \<in> carrier G"