# HG changeset patch
# User paulson
# Date 849087398 -3600
# Node ID f01ac387e82b0f64511583ffa90ef15e117ec587
# Parent  c7869a443b1421b60209709215efba088ca7124d
Replaced obsolete "use" command

diff -r c7869a443b14 -r f01ac387e82b src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
+++ b/src/CTT/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
@@ -20,7 +20,7 @@
 use_thy "Arith";
 use_thy "Bool";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val CTT_build_completed = ();   (*indicate successful build*)
diff -r c7869a443b14 -r f01ac387e82b src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
+++ b/src/Cube/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
@@ -14,7 +14,7 @@
 print_depth 1;  
 use_thy "Cube";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val Cube_build_completed = ();  (*indicate successful build*)
diff -r c7869a443b14 -r f01ac387e82b src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
+++ b/src/FOL/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
@@ -69,7 +69,7 @@
 
 use "simpdata.ML";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val FOL_build_completed = ();   (*indicate successful build*)
diff -r c7869a443b14 -r f01ac387e82b src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Wed Nov 27 10:34:28 1996 +0100
+++ b/src/FOLP/ROOT.ML	Wed Nov 27 10:36:38 1996 +0100
@@ -75,7 +75,7 @@
 
 use "simpdata.ML";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val FOLP_build_completed = ();  (*indicate successful build*)