diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 25 19:03:02 2014 +0100
@@ -6,8 +6,6 @@
   val is_official = false;
 end;
 
-print_depth 10;
-
 
 (* library of general tools *)