diff -r 91dfe7dccfdf -r 3165bc303f66 doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Mon May 31 19:36:13 2010 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Mon May 31 21:06:57 2010 +0200
@@ -10,7 +10,7 @@
 
 
 ML "Pretty.margin_default := 64"
-ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
+ML "Thy_Output.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
 
 
 text {*Now in Basic.thy!