--- a/src/HOL/IsaMakefile Mon Aug 24 17:16:49 1998 +0200
+++ b/src/HOL/IsaMakefile Mon Aug 24 18:17:25 1998 +0200
@@ -295,7 +295,8 @@
ex/IntRing.thy ex/IntRingDefs.ML ex/IntRingDefs.thy ex/Lagrange.ML \
ex/Lagrange.thy ex/Ring.ML ex/Ring.thy ex/StringEx.ML \
ex/StringEx.thy ex/BinEx.ML ex/BinEx.thy ex/MonoidGroup.thy \
- ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML
+ ex/PiSets.thy ex/PiSets.ML ex/LocaleGroup.thy ex/LocaleGroup.ML \
+ ex/Antiquote.thy ex/Antiquote.ML
@$(ISATOOL) usedir $(OUT)/HOL ex