--- a/doc-src/TutorialI/CodeGen/ROOT.ML Mon Sep 04 21:20:14 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/ROOT.ML Tue Sep 05 09:03:17 2000 +0200 @@ -1,1 +1,2 @@ +use "../settings.ML"; use_thy "CodeGen";