doc-src/TutorialI/Fun/ROOT.ML

modifying the depth-limited compilation to be sound, but now throws an error undefined in case of hitting the depth limit in an negative context; cleaning up the examples

use "../settings";
use_thy "fun0";