src/HOL/ROOT.ML
changeset 4864 3abfe2093aa0
parent 4758 35f4ad4f055d
child 4896 4727272f3db6
--- a/src/HOL/ROOT.ML	Wed Apr 29 11:37:58 1998 +0200
+++ b/src/HOL/ROOT.ML	Wed Apr 29 11:38:52 1998 +0200
@@ -35,11 +35,12 @@
 
 use_thy "Ord";
 use_thy "subset";
-use "typedef.ML";
+use "Tools/typedef_package.ML";
 use_thy "Sum";
 use_thy "Gfp";
 
-use "record.ML";
+use "Tools/record_package.ML";
+use_thy "Record";
 
 use "datatype.ML";
 use_thy "Arith";