--- a/src/Pure/ROOT.ML Wed Mar 09 18:44:52 2005 +0100 +++ b/src/Pure/ROOT.ML Thu Mar 10 09:11:57 2005 +0100 @@ -11,7 +11,6 @@ print_depth 10; -error_depth 30; (*fake hiding of private structures*) structure Hidden = struct end;