diff -r fed088a475f9 -r 7ee0529c5674 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:03 2007 +0100
+++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:04 2007 +0100
@@ -12,7 +12,7 @@
 
 
 ML "Pretty.setmargin 64"
-ML "IsarOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
+ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
 text {*Now in Basic.thy!