--- 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;