# HG changeset patch # User berghofe # Date 870820753 -7200 # Node ID 5756c98ebf1fab162ca6528c916edb6929f93fdb # Parent d81caea336ba22264c71ac41a872c602b8e1242a Replaced "init_thy_reader" by "set_parser". diff -r d81caea336ba -r 5756c98ebf1f src/HOLCF/ax_ops/thy_syntax.ML --- a/src/HOLCF/ax_ops/thy_syntax.ML Wed Aug 06 00:37:21 1997 +0200 +++ b/src/HOLCF/ax_ops/thy_syntax.ML Wed Aug 06 00:39:13 1997 +0200 @@ -33,4 +33,4 @@ end; structure ThySyn = ThySynFun(ThySynData); -init_thy_reader (); +set_parser ThySyn.parse;