ROOT.ML

--- a/ROOT.ML	Fri Nov 04 14:17:20 1994 +0100
+++ b/ROOT.ML	Fri Nov 04 14:19:30 1994 +0100
@@ -1,19 +1,22 @@
-(*  Title: 	HOL/ROOT
+(*  Title:      HOL/ROOT.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1993  University of Cambridge
 
-Adds Classical Higher-order Logic to a database containing pure Isabelle. 
+Adds Classical Higher-order Logic to a database containing Pure Isabelle.
 Should be executed in the subdirectory HOL.
 *)
 
 val banner = "Higher-Order Logic";
 writeln banner;
 
-init_thy_reader();
+print_depth 1;
+set eta_contract;
 
-print_depth 1;  
-eta_contract := true;
+(* Add user sections *)
+use "../Pure/section_utils.ML";
+use "thy_syntax.ML";
+
 use_thy "HOL";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
@@ -35,7 +38,7 @@
    (fn prems => [ REPEAT(resolve_tac prems 1) ]);
 
   val rev_mp = rev_mp
-  val subst = subst 
+  val subst = subst
   val sym = sym
   end;
 
@@ -43,12 +46,12 @@
 open Hypsubst;
 
 (** Applying ClassicalFun to create a classical prover **)
-structure Classical_Data = 
+structure Classical_Data =
   struct
   val sizef = size_of_thm
   val mp = mp
   val not_elim = notE
-  val swap = swap
+  val classical = classical
   val hyp_subst_tacs=[hyp_subst_tac]
   end;
 
@@ -60,10 +63,10 @@
                        addSEs [conjE,disjE,impCE,FalseE,iffE];
 
 (*Quantifier rules*)
-val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I] 
+val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,ex1E] addEs [allE];
 
-val HOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I] 
+val HOL_dup_cs = prop_cs addSIs [allI] addIs [exCI,ex1I]
                          addSEs [exE,ex1E] addEs [all_dupE];
 
 structure HOL_Induction = InductionFun(struct val spec=spec end);
@@ -73,13 +76,13 @@
 use_thy "Ord";
 use_thy "subset";
 use_thy "equalities";
+use     "hologic.ML";
+use     "subtype.ML";
 use_thy "Prod";
 use_thy "Sum";
 use_thy "Gfp";
 use_thy "Nat";
 
-(* Add user sections *)
-use "../Pure/section_utils.ML";
 use "datatype.ML";
 use "ind_syntax.ML";
 use "add_ind_def.ML";
@@ -87,20 +90,23 @@
 use "indrule.ML";
 use "Inductive.ML";
 
-structure ThySyn = ThySynFun
- (val user_keywords = ["|", "datatype", "primrec",
-		       "inductive", "coinductive", "intrs", 
-		       "monos", "con_defs"]
-  and user_sections = [("inductive",  inductive_decl ""),
-		       ("coinductive",  inductive_decl "Co"),
-		       ("datatype",  datatype_decls),
-		       ("primrec", primrec_decl)]);
+(* FIXME -> thy_syntax.ML *)
+structure ThySynData =
+struct
+  val user_keywords = ThySynData.user_keywords;
+
+  val user_sections = ThySynData.user_sections @
+   [("datatype", datatype_decls),
+    ("primrec", primrec_decl)];
+end;
+structure ThySyn = ThySynFun(ThySynData);
 init_thy_reader ();
 
+
 use_thy "Finite";
 use_thy "List";
 
-use "../Pure/install_pp.ML";
-print_depth 8;  
+init_pps ();
+print_depth 8;
 
-val HOL_build_completed = ();	(*indicate successful build*)
+val HOL_build_completed = ();   (*indicate successful build*)