--- 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 *)