--- a/src/HOL/ROOT.ML Fri Apr 16 14:49:09 1999 +0200
+++ b/src/HOL/ROOT.ML Fri Apr 16 14:49:34 1999 +0200
@@ -56,12 +56,14 @@
use "Tools/record_package.ML";
use_thy "Record";
+(*TFL: recursive function definitions*)
+use_thy "WF_Rel";
+cd "../TFL";
+use "sys.sml";
+cd "../HOL";
+use "Tools/recdef_package.ML";
+use "Tools/induct_method.ML";
use_thy "Recdef";
-(*TFL: recursive function definitions*)
-cd "~~/src/TFL";
-use "sys.sml";
-cd "~~/src/HOL";
-use "Tools/recdef_package.ML";
cd "Integ";
use_thy "IntDef";