diff -r c0abd2fd9b7c -r d5e1a2b869a2 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Apr 04 13:57:40 1997 +0200
+++ b/src/HOL/IsaMakefile	Fri Apr 04 14:01:18 1997 +0200
@@ -183,6 +183,14 @@
 	@$(ISATOOL) usedir -s AxClasses-Tutorial $(OUT)/HOL AxClasses/Tutorial
 
 
+## Higher-order quotients
+
+QUOT_FILES = Quot/ROOT.ML
+
+Quot:	$(OUT)/HOL $(QUOT_FILES)
+	@$(ISATOOL) usedir $(OUT)/HOL Quot
+
+
 ## Miscellaneous examples
 
 EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
@@ -198,7 +206,7 @@
 ## Full test
 
 test:	$(OUT)/HOL \
-	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses ex
+	TFL IMP Hoare Lex Integ Auth Subst Lambda W0 MiniML IOA AxClasses Quot ex
 	echo 'Test examples ran successfully' > test