src/HOL/ROOT.ML

--- a/src/HOL/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
+++ b/src/HOL/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
@@ -9,8 +9,6 @@
 val banner = "Higher-Order Logic";
 writeln banner;
 
-print_depth 1;
-
 (*old-style theory syntax*)
 use "thy_syntax.ML";
 
@@ -40,8 +38,6 @@
 
 path_add "~~/src/HOL/Library";
 
-print_depth 8;
-
 Goal "True";  (*leave subgoal package empty*)
 
 val HOL_proofs = !proofs;