diff -r 85898be702b2 -r e843c1d6f9e1 src/HOLCF/ROOT.ML
--- a/src/HOLCF/ROOT.ML	Wed Aug 06 11:57:52 1997 +0200
+++ b/src/HOLCF/ROOT.ML	Wed Aug 06 11:58:50 1997 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOLCF/ROOT
+(*  Title:      HOLCF/ROOT.ML
     ID:         $Id$
     Author:     Franz Regensburger
     Copyright   1993 Technische Universitaet Muenchen
@@ -7,14 +7,15 @@
 Should be executed in subdirectory HOLCF.
 *)
 
-val banner = "HOLCF with sections axioms,ops,domain,generated";
+val banner = "HOLCF";
 writeln banner;
 
 print_depth 1;
 
 use_thy "HOLCF";
 
-(* install sections: axioms, ops *)
+
+(* sections axioms, ops *)
 
 use "ax_ops/holcflogic.ML";
 use "ax_ops/thy_axioms.ML";
@@ -22,7 +23,7 @@
 use "ax_ops/thy_syntax.ML";
 
 
-(* install sections: domain, generated *)
+(* sections domain, generated *)
 
 use "domain/library.ML";
 use "domain/syntax.ML";
@@ -31,11 +32,6 @@
 use "domain/extender.ML";
 use "domain/interface.ML";
 
-set_parser ThySyn.parse;
-
-fun qed_spec_mp name =
-  let val thm = normalize_thm [RSspec,RSmp] (result())
-  in bind_thm(name, thm) end;
 
 print_depth 10;