# HG changeset patch
# User ballarin
# Date 1110442317 -3600
# Node ID b5f5722ed703369634f70f50471bbedcb30716c4
# Parent  8665d08085df8a8344db448a15f2eca6df552f7f
Debugging code (error_depth) removed.

diff -r 8665d08085df -r b5f5722ed703 src/Pure/ROOT.ML
--- 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;