# HG changeset patch
# User berghofe
# Date 870821240 -7200
# Node ID 5f4c5fec9994924a4bb3b20f2c344c08d7ec9154
# Parent  403db95b54ff73e90e28ab76a2830f04ed546f64
Replaced "init_thy_reader" by "set_parser".

diff -r 403db95b54ff -r 5f4c5fec9994 src/ZF/thy_syntax.ML
--- a/src/ZF/thy_syntax.ML	Wed Aug 06 00:45:09 1997 +0200
+++ b/src/ZF/thy_syntax.ML	Wed Aug 06 00:47:20 1997 +0200
@@ -151,4 +151,4 @@
 
 
 structure ThySyn = ThySynFun(ThySynData);
-init_thy_reader ();
+set_parser ThySyn.parse;