Replaced "init_thy_reader" by "set_parser".
--- a/src/HOL/thy_syntax.ML Wed Aug 06 01:17:42 1997 +0200
+++ b/src/HOL/thy_syntax.ML Wed Aug 06 01:18:31 1997 +0200
@@ -278,5 +278,5 @@
structure ThySyn = ThySynFun(ThySynData);
-init_thy_reader ();
+set_parser ThySyn.parse;