diff -r 37a92211a5d3 -r dbb95b825244 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:06:52 2004 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Apr 16 04:07:10 2004 +0200
@@ -5,9 +5,9 @@
   Copyright: Clemens Ballarin
 *)
 
-theory UnivPoly = Module:
+header {* Univariate Polynomials *}
 
-section {* Univariate Polynomials *}
+theory UnivPoly = Module:
 
 text {*
   Polynomials are formalised as modules with additional operations for