# HG changeset patch
# User paulson
# Date 849095952 -3600
# Node ID d388a38f7198ae6d7508163b51230c70c501037b
# Parent  fce7e34db8c863eda4bb5f72486cbfd1b56b3acb
Replaced obsolete "use" command

diff -r fce7e34db8c8 -r d388a38f7198 src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Wed Nov 27 12:56:11 1996 +0100
+++ b/src/Sequents/ROOT.ML	Wed Nov 27 12:59:12 1996 +0100
@@ -24,7 +24,7 @@
 use_thy"S4";
 use_thy"S43";
 
-use "../Pure/install_pp.ML";
+init_pps ();
 print_depth 8;
 
 val Sequents_build_completed = ();    (*indicate successful build*)