# HG changeset patch
# User wenzelm
# Date 908893514 -7200
# Node ID 9a3acc4c7c2eb902caea41ea29468c0b11924e3d
# Parent  e62518aacc5b60ad8c416b83672c6ed1f58bc17f
structure Hidden = struct end;

diff -r e62518aacc5b -r 9a3acc4c7c2e 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";