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