# HG changeset patch
# User wenzelm
# Date 868460434 -7200
# Node ID da4dd8b7ced4c04b91f1dfdeaa887dc2e5c870df
# Parent  24d235feeb2a9da9ca272a57e9f8d2c0d2211f12
removed obsolete init_pps and init_thy_reader;

diff -r 24d235feeb2a -r da4dd8b7ced4 NEWS
--- a/NEWS	Wed Jul 09 16:54:17 1997 +0200
+++ b/NEWS	Wed Jul 09 17:00:34 1997 +0200
@@ -7,6 +7,8 @@
 
 * removed old README and Makefiles;
 
+* removed obsolete init_pps and init_database;
+
 
 New in Isabelle94-8 (May 1997)
 ------------------------------
diff -r 24d235feeb2a -r da4dd8b7ced4 src/CTT/ROOT.ML
--- a/src/CTT/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/CTT/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -12,15 +12,12 @@
 
 print_depth 1;  
 
-init_thy_reader();
-
 use_thy "CTT";
 use "../Provers/typedsimp.ML";
 use "rew.ML";
 use_thy "Arith";
 use_thy "Bool";
 
-init_pps ();
 print_depth 8;
 
 val CTT_build_completed = ();   (*indicate successful build*)
diff -r 24d235feeb2a -r da4dd8b7ced4 src/Cube/ROOT.ML
--- a/src/Cube/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/Cube/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -1,20 +1,18 @@
-(*  Title:      Cube/ROOT
+(*  Title:      Cube/ROOT.ML
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   1992  University of Cambridge
 
-The Lambda-Cube a la Barendregt
+The Lambda-Cube a la Barendregt.
 *)
 
 val banner = "Barendregt's Lambda-Cube";
 writeln banner;
 
-init_thy_reader();
+print_depth 1;  
 
-print_depth 1;  
 use_thy "Cube";
 
-init_pps ();
 print_depth 8;
 
 val Cube_build_completed = ();  (*indicate successful build*)
diff -r 24d235feeb2a -r da4dd8b7ced4 src/FOL/ROOT.ML
--- a/src/FOL/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/FOL/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -11,8 +11,6 @@
 
 writeln banner;
 
-init_thy_reader();
-
 print_depth 1;  
 
 use "../Provers/splitter.ML";
@@ -49,7 +47,6 @@
  (fn _ => [ (deepen_tac FOL_cs 0 1) ]);
 
 
-init_pps ();
 print_depth 8;
 
 val FOL_build_completed = ();   (*indicate successful build*)
diff -r 24d235feeb2a -r da4dd8b7ced4 src/FOLP/ROOT.ML
--- a/src/FOLP/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/FOLP/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -12,9 +12,8 @@
 
 writeln banner;
 
-init_thy_reader();
+print_depth 1;
 
-print_depth 1;  
 use_thy "IFOLP";
 use_thy "FOLP";
 
@@ -75,7 +74,7 @@
 
 use "simpdata.ML";
 
-init_pps ();
+
 print_depth 8;
 
 val FOLP_build_completed = ();  (*indicate successful build*)
diff -r 24d235feeb2a -r da4dd8b7ced4 src/HOL/Auth/DB-ROOT.ML
--- a/src/HOL/Auth/DB-ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/HOL/Auth/DB-ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -12,7 +12,4 @@
 val banner = "Security Protocols";
 writeln banner;
 
-init_thy_reader();
-
 use_thy "Message";
-
diff -r 24d235feeb2a -r da4dd8b7ced4 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/HOL/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -49,7 +49,6 @@
 use "sys.sml";
 cd "../HOL";
 
-init_pps ();
 print_depth 8;
 
 val HOL_build_completed = ();   (*indicate successful build*)
diff -r 24d235feeb2a -r da4dd8b7ced4 src/HOL/thy_data.ML
--- a/src/HOL/thy_data.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/HOL/thy_data.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -106,7 +106,7 @@
 end;
 
 (*Must be redefined in order to refer to the new instance of bind_thm
-  created by init_thy_reader.*)
+  created by init_thy_reader.*)		(* FIXME: move *)
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())
diff -r 24d235feeb2a -r da4dd8b7ced4 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/HOLCF/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -32,7 +32,6 @@
 use "domain/interface.ML";
 
 init_thy_reader();
-init_pps ();
 
 fun qed_spec_mp name =
   let val thm = normalize_thm [RSspec,RSmp] (result())
diff -r 24d235feeb2a -r da4dd8b7ced4 src/Sequents/ROOT.ML
--- a/src/Sequents/ROOT.ML	Wed Jul 09 16:54:17 1997 +0200
+++ b/src/Sequents/ROOT.ML	Wed Jul 09 17:00:34 1997 +0200
@@ -9,8 +9,6 @@
 val banner = "Sequent Calculii";
 writeln banner;
 
-init_thy_reader();
-
 print_depth 1;  
 
 use_thy "Sequents";
@@ -24,7 +22,6 @@
 use_thy"S4";
 use_thy"S43";
 
-init_pps ();
 print_depth 8;
 
 val Sequents_build_completed = ();    (*indicate successful build*)