src/HOL/thy_syntax.ML
changeset 3617 b689656214ea
parent 3456 fdb1768ebd3e
child 3622 85898be702b2
     1.1 --- a/src/HOL/thy_syntax.ML	Wed Aug 06 01:17:42 1997 +0200
     1.2 +++ b/src/HOL/thy_syntax.ML	Wed Aug 06 01:18:31 1997 +0200
     1.3 @@ -278,5 +278,5 @@
     1.4  
     1.5  
     1.6  structure ThySyn = ThySynFun(ThySynData);
     1.7 -init_thy_reader ();
     1.8 +set_parser ThySyn.parse;
     1.9