diff -r 59d5fe89f787 -r 9712294e60b9 doc-src/Tutorial/IsaMakefile
--- a/doc-src/Tutorial/IsaMakefile	Thu Nov 12 11:27:36 1998 +0100
+++ b/doc-src/Tutorial/IsaMakefile	Thu Nov 12 16:45:17 1998 +0100
@@ -4,7 +4,7 @@
 
 ## targets
 
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Misc
+default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Misc
 
 
 ## global settings
@@ -62,6 +62,32 @@
   CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML
 	@$(ISATOOL) usedir $(OUT)/HOL CodeGen
 
+## HOL-Datatype
+
+HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
+
+Datatype/appmap.ML: Datatype/appmap
+	cat Datatype/goal Datatype/appmap Datatype/semi > Datatype/appmap.ML
+
+Datatype/ABexp.thy: Datatype/abprolog Datatype/abdata Datatype/abconstseval \
+  Datatype/abevala Datatype/abevalb Datatype/abconstssubst Datatype/absubsta\
+  Datatype/absubstb
+	cd Datatype; cat abprolog abdata abconstseval abevala abevalb abconstssubst absubsta absubstb end > ABexp.thy
+
+Datatype/Term.thy: Datatype/tprolog Datatype/mutnested Datatype/tdata \
+  Datatype/tconstssubst Datatype/tsubst Datatype/tsubsts
+	cd Datatype; cat tprolog mutnested tdata tconstssubst tsubst tsubsts end > Term.thy
+
+Datatype/Trie.thy: Datatype/trieprolog Datatype/assoc Datatype/trie \
+  Datatype/triesels Datatype/lookup Datatype/update
+	cd Datatype; cat trieprolog assoc trie triesels lookup update end > Trie.thy
+
+$(LOG)/HOL-Datatype.gz: $(OUT)/HOL \
+  Datatype/ABexp.thy Datatype/Term.thy Datatype/Trie.thy \
+  Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
+  Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
+  Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
+	@$(ISATOOL) usedir $(OUT)/HOL Datatype
 
 ## HOL-Misc