# HG changeset patch
# User wenzelm
# Date 1119298436 -7200
# Node ID ace3c2b9535327b53947fbeaf2640549b7d847df
# Parent  ed08c8edc2897e2551d9902c53683640c428f037
removed obsolete print_depth;

diff -r ed08c8edc289 -r ace3c2b95353 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
+++ b/src/FOL/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
@@ -8,8 +8,6 @@
 
 writeln banner;
 
-print_depth 1;  
-
 use "~~/src/Provers/splitter.ML";
 use "~~/src/Provers/ind.ML";
 use "~~/src/Provers/hypsubst.ML";
@@ -21,5 +19,3 @@
 use "~~/src/Provers/quantifier1.ML";
 
 use_thy "FOL";
-
-print_depth 8;
diff -r ed08c8edc289 -r ace3c2b95353 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;
diff -r ed08c8edc289 -r ace3c2b95353 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
+++ b/src/HOLCF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
@@ -8,8 +8,6 @@
 val banner = "HOLCF";
 writeln banner;
 
-print_depth 1;
-
 use_thy "HOLCF";
 
 use "holcf_logic.ML";
@@ -24,5 +22,3 @@
 use "domain/interface.ML";
 
 path_add "~~/src/HOLCF/ex";
-
-print_depth 10;  
diff -r ed08c8edc289 -r ace3c2b95353 src/ZF/ROOT.ML
--- a/src/ZF/ROOT.ML	Mon Jun 20 22:13:55 2005 +0200
+++ b/src/ZF/ROOT.ML	Mon Jun 20 22:13:56 2005 +0200
@@ -13,13 +13,9 @@
 
 reset eta_contract;
 
-print_depth 1;
-
 (*syntax for old-style theory sections*)
 use "thy_syntax";
 
 with_path "Integ" use_thy "Main_ZFC";
 
-print_depth 8;
-
 Goal "True";  (*leave subgoal package empty*)