--- a/src/HOL/Algebra/RingHom.thy Fri Dec 19 14:31:07 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy Fri Dec 19 14:31:17 2008 +0100
@@ -17,10 +17,10 @@
notes hom_mult [simp] = ring_hom_mult [OF homh]
and hom_one [simp] = ring_hom_one [OF homh]
-sublocale ring_hom_cring \<subseteq> ring_hom_ring
+sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
proof qed (rule homh)
-sublocale ring_hom_ring \<subseteq> abelian_group_hom R S
+sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
apply (rule abelian_group_homI)
apply (rule R.is_abelian_group)
apply (rule S.is_abelian_group)