src/Pure/ROOT.ML
changeset 5684 9a3acc4c7c2e
parent 5607 5db9e2343ade
child 5834 c6fea8488ce7
--- 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";