src/HOLCF/ROOT.ML
changeset 3608 d81caea336ba
parent 3511 da4dd8b7ced4
child 3623 e843c1d6f9e1
     1.1 --- a/src/HOLCF/ROOT.ML	Wed Aug 06 00:33:13 1997 +0200
     1.2 +++ b/src/HOLCF/ROOT.ML	Wed Aug 06 00:37:21 1997 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  use "domain/extender.ML";
     1.5  use "domain/interface.ML";
     1.6  
     1.7 -init_thy_reader();
     1.8 +set_parser ThySyn.parse;
     1.9  
    1.10  fun qed_spec_mp name =
    1.11    let val thm = normalize_thm [RSspec,RSmp] (result())