src/Pure/ROOT.ML

--- 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";