diff -r d5c6d1fb236b -r 74ce9774c923 ROOT.ML
--- a/ROOT.ML	Fri Nov 25 13:33:27 1994 +0100
+++ b/ROOT.ML	Fri Nov 25 13:34:33 1994 +0100
@@ -22,7 +22,6 @@
 use "../Provers/classical.ML";
 use "../Provers/simplifier.ML";
 use "../Provers/splitter.ML";
-use "../Provers/ind.ML";
 
 (** Applying HypsubstFun to generate hyp_subst_tac **)
 
@@ -60,9 +59,6 @@
 val HOL_cs = prop_cs addSIs [allI] addIs [exI,ex1I]
                      addSEs [exE,ex1E] addEs [allE];
 
-structure HOL_Induction = InductionFun(struct val spec=spec end);
-open HOL_Induction;
-
 use     "simpdata.ML";
 use_thy "Ord";
 use_thy "subset";
@@ -79,7 +75,7 @@
 use "add_ind_def.ML";
 use "intr_elim.ML";
 use "indrule.ML";
-use "Inductive.ML";
+use_thy "Inductive";
 
 use_thy "Finite";
 use_thy "List";