diff -r b963e9cee2a0 -r 5cf13e80be0e src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Nov 25 10:37:03 2003 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 27 10:47:55 2003 +0100
@@ -147,8 +147,8 @@
   Real/RealBin.thy Real/RealDef.ML Real/RealDef.thy Real/RealInt.ML \
   Real/RealInt.thy Real/RealOrd.thy \
   Real/RealPow.thy Real/document/root.tex Real/real_arith.ML\
-  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy Hyperreal/ExtraThms2.ML\
-  Hyperreal/ExtraThms2.thy Hyperreal/Fact.ML Hyperreal/Fact.thy\
+  Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
+  Hyperreal/Fact.ML Hyperreal/Fact.thy\
   Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
   Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\