--- a/src/HOL/ROOT.ML Tue Sep 21 11:11:09 1999 +0200 +++ b/src/HOL/ROOT.ML Tue Sep 21 14:13:45 1999 +0200 @@ -56,7 +56,6 @@ use_thy "IntDef"; use "simproc.ML"; use_thy "NatBin"; -use "bin_simprocs.ML"; cd ".."; (*the all-in-one theory*)