Replaced obsolete "use" command
authorpaulson
Wed Nov 27 12:59:12 1996 +0100 (1996-11-27)
changeset 2247d388a38f7198
parent 2246 fce7e34db8c8
child 2248 187d001fbe79
Replaced obsolete "use" command
src/Sequents/ROOT.ML
     1.1 --- a/src/Sequents/ROOT.ML	Wed Nov 27 12:56:11 1996 +0100
     1.2 +++ b/src/Sequents/ROOT.ML	Wed Nov 27 12:59:12 1996 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  use_thy"S4";
     1.5  use_thy"S43";
     1.6  
     1.7 -use "../Pure/install_pp.ML";
     1.8 +init_pps ();
     1.9  print_depth 8;
    1.10  
    1.11  val Sequents_build_completed = ();    (*indicate successful build*)