diff -r 97c1d5c7b701 -r 1ce3cccfacdb src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Jul 03 17:34:55 1998 +0200
+++ b/src/HOL/ROOT.ML	Fri Jul 03 17:35:39 1998 +0200
@@ -52,7 +52,7 @@
 use_thy "RelPow";
 use_thy "Finite";
 use_thy "Sexp";
-use_thy "WF_Rel";
+use_thy "Recdef";
 use_thy "Map";
 use_thy "Update";
 
@@ -65,6 +65,9 @@
 use "sys.sml";
 cd "$ISABELLE_HOME/src/HOL";
 
+(*the all-in-one theory*)
+use_thy "Main";
+
 print_depth 8;
 
 val HOL_build_completed = ();   (*indicate successful build*)