diff -r d649506f40c3 -r 29bb4659f80a src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Tue Jul 04 12:13:38 2006 +0200
+++ b/src/HOL/Algebra/Module.thy	Tue Jul 04 14:47:01 2006 +0200
@@ -73,7 +73,7 @@
       "!!a x y. [| a \<in> carrier R; x \<in> carrier M; y \<in> carrier M |] ==>
       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
   shows "algebra R M"
-apply (intro_locales!)
+apply intro_locales
 apply (rule cring.axioms ring.axioms abelian_group.axioms comm_monoid.axioms prems)+
 apply (rule module_axioms.intro)
  apply (simp add: smult_closed)
@@ -88,11 +88,11 @@
 
 lemma (in algebra) R_cring:
   "cring R"
-  by intro_locales
+  by unfold_locales
 
 lemma (in algebra) M_cring:
   "cring M"
-  by intro_locales
+  by unfold_locales
 
 lemma (in algebra) module:
   "module R M"