# HG changeset patch
# User berghofe
# Date 870823111 -7200
# Node ID b689656214eafba0a4724ce1d0d2891c0e6412a4
# Parent  fcd7e70258f7178a9845396caf73f16106d8bc69
Replaced "init_thy_reader" by "set_parser".

diff -r fcd7e70258f7 -r b689656214ea src/HOL/thy_syntax.ML
--- 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;