src/HOL/Algebra/RingHom.thy

--- a/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/RingHom.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -17,7 +17,7 @@
     and hom_one [simp] = ring_hom_one [OF homh]
 
 sublocale ring_hom_cring \<subseteq> ring: ring_hom_ring
-  by default (rule homh)
+  by standard (rule homh)
 
 sublocale ring_hom_ring \<subseteq> abelian_group: abelian_group_hom R S
 apply (rule abelian_group_homI)