src/LCF/ROOT.ML
changeset 4905 be73ddff6c5a
parent 4024 3c056eab237c
child 6349 f7750d816c21
--- a/src/LCF/ROOT.ML	Fri May 08 10:15:39 1998 +0200
+++ b/src/LCF/ROOT.ML	Fri May 08 13:54:45 1998 +0200
@@ -14,7 +14,7 @@
 print_depth 1;
 use_thy "LCF";
 use"simpdata.ML";
-use"pair.ML";
-use"fix.ML";
+use_thy"pair";
+use_thy"fix";
 
 val LCF_build_completed = ();   (*indicate successful build*)