diff -r 187b73f64023 -r 8c0c3a67d9e1 ROOT.ML
--- a/ROOT.ML	Tue Nov 09 16:31:03 1993 +0100
+++ b/ROOT.ML	Tue Nov 16 14:14:22 1993 +0100
@@ -15,7 +15,7 @@
 
 print_depth 1;  
 eta_contract := true;
-use_thy "hol";
+use_thy "HOL";
 use "../Provers/hypsubst.ML";
 use "../Provers/classical.ML";
 use "../Provers/simplifier.ML";
@@ -71,24 +71,24 @@
 open HOL_Induction;
 
 use     "simpdata.ML";
-use_thy "ord";
-use_thy "set";
+use_thy "Ord";
+use_thy "Set";
 use     "fun.ML";
 use     "subset.ML";
 use     "equalities.ML";
-use_thy "prod";
-use_thy "sum";
+use_thy "Prod";
+use_thy "Sum";
 use     "mono.ML";
-use_thy "lfp";
-use_thy "gfp";
-use_thy "trancl";
-use_thy "wf";
-use_thy "nat";
-use_thy "arith";
-use_thy "univ";
-use_thy "sexp";
-use_thy "list";
-use_thy "llist";
+use_thy "Lfp";
+use_thy "Gfp";
+use_thy "Trancl";
+use_thy "WF";
+use_thy "Nat";
+use_thy "Arith";
+use_thy "Univ";
+use_thy "Sexp";
+use_thy "List";
+use_thy "LList";
 
 use "../Pure/install_pp.ML";
 print_depth 8;