diff -r c0489217deb2 -r f508492af9b4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Dec 22 12:50:01 2003 +0100
+++ b/src/HOL/IsaMakefile	Mon Dec 22 12:50:22 2003 +0100
@@ -150,7 +150,7 @@
   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\
+  Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
   Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\