diff -r 55b80ec1927d -r c3f3fd86e11c src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Jul 23 16:54:28 1999 +0200
+++ b/src/HOL/ROOT.ML	Fri Jul 23 17:24:48 1999 +0200
@@ -27,10 +27,12 @@
 use "~~/src/Provers/Arith/cancel_sums.ML";
 use "~~/src/Provers/Arith/cancel_factor.ML";
 use "~~/src/Provers/Arith/abel_cancel.ML";
+use "~~/src/Provers/Arith/assoc_fold.ML";
 use "~~/src/Provers/quantifier1.ML";
 
 use_thy "HOL";
 use "hologic.ML";
+use "~~/src/Provers/Arith/combine_coeff.ML";
 use "cladata.ML";
 use "simpdata.ML";
 
@@ -70,6 +72,7 @@
 use_thy "IntDef";
 use "simproc.ML";
 use_thy "NatBin";
+use "bin_simprocs.ML";
 cd "..";
 
 (*the all-in-one theory*)