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