diff -r 7ca11ecbc4fb -r dcbef866c9e2 src/HOL/Algebra/RingHom.thy
--- a/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:27 2008 +0100
+++ b/src/HOL/Algebra/RingHom.thy	Mon Nov 17 17:00:55 2008 +0100
@@ -17,7 +17,7 @@
     and hom_one [simp] = ring_hom_one [OF homh]
 
 interpretation ring_hom_cring \<subseteq> ring_hom_ring
-  by (unfold_locales, rule homh)
+  proof qed (rule homh)
 
 interpretation ring_hom_ring \<subseteq> abelian_group_hom R S
 apply (rule abelian_group_homI)