diff -r 3879dc0e9a9c -r c5c4884634b7 src/HOL/Complex/ex/Sqrt_Script.thy
--- a/src/HOL/Complex/ex/Sqrt_Script.thy	Thu Aug 19 10:33:10 2004 +0200
+++ b/src/HOL/Complex/ex/Sqrt_Script.thy	Thu Aug 19 12:35:45 2004 +0200
@@ -6,7 +6,9 @@
 
 header {* Square roots of primes are irrational (script version) *}
 
-theory Sqrt_Script = Primes + Complex_Main:
+theory Sqrt_Script
+imports Primes Complex_Main
+begin
 
 text {*
   \medskip Contrast this linear Isabelle/Isar script with Markus