diff -r 48c4632e2c28 -r 82f365a14960 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Tue Jun 06 09:28:24 2006 +0200
+++ b/src/HOL/Algebra/Module.thy	Tue Jun 06 10:05:57 2006 +0200
@@ -32,7 +32,7 @@
       (a \<odot>\<^bsub>M\<^esub> x) \<otimes>\<^bsub>M\<^esub> y = a \<odot>\<^bsub>M\<^esub> (x \<otimes>\<^bsub>M\<^esub> y)"
 
 lemma moduleI:
-  includes struct R + struct M
+  fixes R (structure) and M (structure)
   assumes cring: "cring R"
     and abelian_group: "abelian_group M"
     and smult_closed:
@@ -53,7 +53,7 @@
     module_axioms.intro prems)
 
 lemma algebraI:
-  includes struct R + struct M
+  fixes R (structure) and M (structure)
   assumes R_cring: "cring R"
     and M_cring: "cring M"
     and smult_closed: