--- a/ROOT.ML Thu Aug 25 11:01:45 1994 +0200
+++ b/ROOT.ML Tue Aug 30 10:04:49 1994 +0200
@@ -79,8 +79,8 @@
use_thy "Nat";
(* Add user sections *)
-use "Datatype.ML";
use "../Pure/section_utils.ML";
+use "datatype.ML";
use "ind_syntax.ML";
use "add_ind_def.ML";
use "intr_elim.ML";