diff -r 3730ae0f513a -r 4d4521cbbcca src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jun 07 12:06:36 2000 +0200
+++ b/src/HOL/IsaMakefile	Wed Jun 07 12:07:07 2000 +0200
@@ -79,7 +79,7 @@
   Real/PNat.thy Real/PRat.ML Real/PRat.thy Real/PReal.ML \
   Real/PReal.thy Real/RComplete.ML Real/RComplete.thy Real/Real.thy \
   Real/RealDef.ML Real/RealDef.thy Real/RealOrd.ML Real/RealOrd.thy \
-  Real/simproc.ML Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
+  Real/RealAbs.ML Real/RealAbs.thy Real/ROOT.ML \
   Real/RealBin.ML Real/RealBin.thy Real/RealInt.ML Real/RealInt.thy \
   Real/RealPow.ML Real/RealPow.thy Real/Hyperreal/Filter.ML \
   Real/Hyperreal/Filter.thy Real/Hyperreal/fuf.ML \