--- a/src/Pure/ROOT.ML Tue Oct 20 16:24:45 1998 +0200
+++ b/src/Pure/ROOT.ML Tue Oct 20 16:25:14 1998 +0200
@@ -12,6 +12,8 @@
print_depth 1;
ml_prompts "> " "# ";
+(*fake hiding of private structures*)
+structure Hidden = struct end;
(*basic tools*)
use "library.ML";