doc-src/TutorialI/settings.ML

reverted change introduced in a7c164e228e1 -- there cannot be a "bug" in a perfectly normal operation on the internal data representation that merely escaped into public by accident (cf. 0a981c596372);

(* $Id$ *)

ThyOutput.indent := 5;