--- a/src/HOL/Lambda/ROOT.ML Thu Apr 22 18:23:45 1999 +0200
+++ b/src/HOL/Lambda/ROOT.ML Thu Apr 22 18:25:07 1999 +0200
@@ -7,5 +7,5 @@
writeln"Root file for HOL/Lambda";
time_use_thy "Eta";
-add_path "../Induct";
+time_use_thy "../Induct/Acc";
time_use_thy "InductTermi";
--- a/src/HOL/Real/ROOT.ML Thu Apr 22 18:23:45 1999 +0200
+++ b/src/HOL/Real/ROOT.ML Thu Apr 22 18:25:07 1999 +0200
@@ -10,9 +10,7 @@
set proof_timing;
time_use_thy "RealDef";
-use "simproc";
+use "simproc.ML";
time_use_thy "RealAbs";
time_use_thy "RComplete";
-
-add_path "Hyperreal";
-use_thy "Filter";
+time_use_thy "Hyperreal/Filter";