diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/Module.thy
--- a/src/HOL/Algebra/Module.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/Module.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -4,9 +4,9 @@
     Copyright:  Clemens Ballarin
 *)
 
-theory Module = CRing:
+header {* Modules over an Abelian Group *}
 
-section {* Modules over an Abelian Group *}
+theory Module = CRing:
 
 record ('a, 'b) module = "'b ring" +
   smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70)