src/Pure/ROOT.ML
changeset 56281 03c3d1a7c3b8
parent 56229 f61eaab6bec3
child 56287 ca090ae5f258
--- 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 *)