author | berghofe |
Wed, 06 Aug 1997 00:37:21 +0200 | |
changeset 3608 | d81caea336ba |
parent 3607 | a4b9ed94907a |
child 3609 | 5756c98ebf1f |
src/HOLCF/ROOT.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOLCF/ROOT.ML Wed Aug 06 00:33:13 1997 +0200 +++ b/src/HOLCF/ROOT.ML Wed Aug 06 00:37:21 1997 +0200 @@ -31,7 +31,7 @@ use "domain/extender.ML"; use "domain/interface.ML"; -init_thy_reader(); +set_parser ThySyn.parse; fun qed_spec_mp name = let val thm = normalize_thm [RSspec,RSmp] (result())