doc-src/TutorialI/settings.ML

--- a/doc-src/TutorialI/settings.ML	Mon May 31 19:36:13 2010 +0200
+++ b/doc-src/TutorialI/settings.ML	Mon May 31 21:06:57 2010 +0200
@@ -1,3 +1,3 @@
 (* $Id$ *)
 
-ThyOutput.indent := 5;
+Thy_Output.indent := 5;