1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:03 2007 +0100
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Fri Jan 19 22:08:04 2007 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  
     1.6  ML "Pretty.setmargin 64"
     1.7 -ML "IsarOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
     1.8 +ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
     1.9  
    1.10  
    1.11  text {*Now in Basic.thy!