Replaced "init_thy_reader" by set_parser.
authorberghofe
Wed, 06 Aug 1997 00:37:21 +0200
changeset 3608 d81caea336ba
parent 3607 a4b9ed94907a
child 3609 5756c98ebf1f
Replaced "init_thy_reader" by set_parser.
src/HOLCF/ROOT.ML
--- 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())