diff -r de96f2982d2c -r 39d0cc787d47 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue May 23 12:36:36 2000 +0200
+++ b/src/HOL/IsaMakefile	Tue May 23 12:44:03 2000 +0200
@@ -237,6 +237,7 @@
 HOL-UNITY: HOL $(LOG)/HOL-UNITY.gz
 
 $(LOG)/HOL-UNITY.gz: $(OUT)/HOL UNITY/ROOT.ML\
+  UNITY/AllocBase.ML UNITY/AllocBase.thy\
   UNITY/Alloc.ML UNITY/Alloc.thy\
   UNITY/Channel.ML UNITY/Channel.thy UNITY/Common.ML UNITY/Common.thy\
   UNITY/Client.ML UNITY/Client.thy  UNITY/Comp.ML UNITY/Comp.thy\
@@ -410,7 +411,7 @@
 
 $(LOG)/HOL-ex.gz: $(OUT)/HOL  ex/AVL.ML ex/AVL.thy ex/BT.ML ex/BT.thy \
   ex/InSort.ML ex/InSort.thy ex/MT.ML ex/MT.thy ex/NatSum.ML \
-  ex/NatSum.thy ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
+  ex/Fib.ML ex/Fib.thy ex/Primes.ML ex/Primes.thy \
   ex/Factorization.ML ex/Factorization.thy \
   ex/Primrec.ML ex/Primrec.thy \
   ex/Puzzle.ML ex/Puzzle.thy ex/Qsort.ML ex/Qsort.thy \