src/ZF/thy_syntax.ML
changeset 3613 5f4c5fec9994
parent 3399 0c4efa9eac29
child 3622 85898be702b2
equal deleted inserted replaced
3612:403db95b54ff 3613:5f4c5fec9994
   149                      ("codatatype",  datatype_decl "Co")];
   149                      ("codatatype",  datatype_decl "Co")];
   150 end;
   150 end;
   151 
   151 
   152 
   152 
   153 structure ThySyn = ThySynFun(ThySynData);
   153 structure ThySyn = ThySynFun(ThySynData);
   154 init_thy_reader ();
   154 set_parser ThySyn.parse;