Replaced obsolete "use" command
authorpaulson
Wed Nov 27 10:36:38 1996 +0100 (1996-11-27)
changeset 2237f01ac387e82b
parent 2236 c7869a443b14
child 2238 c72a23bbe762
Replaced obsolete "use" command
src/CTT/ROOT.ML
src/Cube/ROOT.ML
src/FOL/ROOT.ML
src/FOLP/ROOT.ML
     1.1 --- a/src/CTT/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
     1.2 +++ b/src/CTT/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  use_thy "Arith";
     1.5  use_thy "Bool";
     1.6  
     1.7 -use "../Pure/install_pp.ML";
     1.8 +init_pps ();
     1.9  print_depth 8;
    1.10  
    1.11  val CTT_build_completed = ();   (*indicate successful build*)
     2.1 --- a/src/Cube/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
     2.2 +++ b/src/Cube/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  print_depth 1;  
     2.5  use_thy "Cube";
     2.6  
     2.7 -use "../Pure/install_pp.ML";
     2.8 +init_pps ();
     2.9  print_depth 8;
    2.10  
    2.11  val Cube_build_completed = ();  (*indicate successful build*)
     3.1 --- a/src/FOL/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
     3.2 +++ b/src/FOL/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
     3.3 @@ -69,7 +69,7 @@
     3.4  
     3.5  use "simpdata.ML";
     3.6  
     3.7 -use "../Pure/install_pp.ML";
     3.8 +init_pps ();
     3.9  print_depth 8;
    3.10  
    3.11  val FOL_build_completed = ();   (*indicate successful build*)
     4.1 --- a/src/FOLP/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
     4.2 +++ b/src/FOLP/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
     4.3 @@ -75,7 +75,7 @@
     4.4  
     4.5  use "simpdata.ML";
     4.6  
     4.7 -use "../Pure/install_pp.ML";
     4.8 +init_pps ();
     4.9  print_depth 8;
    4.10  
    4.11  val FOLP_build_completed = ();  (*indicate successful build*)