do not change global_names flag;
authorwenzelm
Tue Oct 28 17:41:15 1997 +0100 (1997-10-28)
changeset 40243c056eab237c
parent 4023 a9dc0484c903
child 4025 77e426be5624
do not change global_names flag;
src/Cube/ROOT.ML
src/FOL/ROOT.ML
src/FOLP/ROOT.ML
src/HOL/ROOT.ML
src/LCF/ROOT.ML
     1.1 --- a/src/Cube/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     1.2 +++ b/src/Cube/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     1.3 @@ -9,8 +9,6 @@
     1.4  val banner = "Barendregt's Lambda-Cube";
     1.5  writeln banner;
     1.6  
     1.7 -reset global_names;
     1.8 -
     1.9  print_depth 1;  
    1.10  
    1.11  use_thy "Cube";
     2.1 --- a/src/FOL/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     2.2 +++ b/src/FOL/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     2.3 @@ -11,8 +11,6 @@
     2.4  
     2.5  writeln banner;
     2.6  
     2.7 -reset global_names;
     2.8 -
     2.9  print_depth 1;  
    2.10  
    2.11  use "../Provers/simplifier.ML";
     3.1 --- a/src/FOLP/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     3.2 +++ b/src/FOLP/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     3.3 @@ -12,8 +12,6 @@
     3.4  
     3.5  writeln banner;
     3.6  
     3.7 -reset global_names;
     3.8 -
     3.9  print_depth 1;
    3.10  
    3.11  use_thy "IFOLP";
     4.1 --- a/src/HOL/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     4.2 +++ b/src/HOL/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     4.3 @@ -10,8 +10,6 @@
     4.4  val banner = "Higher-Order Logic";
     4.5  writeln banner;
     4.6  
     4.7 -reset global_names;
     4.8 -
     4.9  print_depth 1;
    4.10  
    4.11  (* Add user sections *)
     5.1 --- a/src/LCF/ROOT.ML	Tue Oct 28 17:37:46 1997 +0100
     5.2 +++ b/src/LCF/ROOT.ML	Tue Oct 28 17:41:15 1997 +0100
     5.3 @@ -11,8 +11,6 @@
     5.4  val banner = "Logic for Computable Functions (in FOL)";
     5.5  writeln banner;
     5.6  
     5.7 -reset global_names;
     5.8 -
     5.9  print_depth 1;
    5.10  use_thy "LCF";
    5.11  use"simpdata.ML";