# HG changeset patch
# User berghofe
# Date 870820641 -7200
# Node ID d81caea336ba22264c71ac41a872c602b8e1242a
# Parent  a4b9ed94907a43b1fd99b451841f856d55a6e079
Replaced "init_thy_reader" by set_parser.

diff -r a4b9ed94907a -r d81caea336ba 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())