diff -r 89669c58e506 -r 0bba840aa07c ROOT.ML
--- 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";