diff -r d9527f97246e -r 89669c58e506 Makefile
--- a/Makefile	Thu Aug 25 10:47:33 1994 +0200
+++ b/Makefile	Thu Aug 25 11:01:45 1994 +0200
@@ -23,15 +23,18 @@
 	equalities.thy equalities.ML \
 	Prod.thy Prod.ML Sum.thy Sum.ML WF.thy WF.ML \
 	mono.thy mono.ML Lfp.thy Lfp.ML Gfp.thy Gfp.ML Nat.thy Nat.ML \
+	add_ind_def.ML ind_syntax.ML indrule.ML Inductive.ML \
+	intr_elim.ML Datatype.ML ../Pure/section_utils.ML\
+	Finite.ML Finite.thy\
         Arith.thy Arith.ML Sexp.thy Sexp.ML Univ.thy Univ.ML \
         LList.thy LList.ML List.thy List.ML \
-	Datatype.ML \
 	../Provers/classical.ML ../Provers/simplifier.ML \
 	../Provers/splitter.ML ../Provers/ind.ML
 
-EX_FILES = ex/ROOT.ML ex/cla.ML ex/Finite.ML ex/Finite.thy\
+EX_FILES = ex/ROOT.ML ex/cla.ML \
 	   ex/LexProd.ML ex/LexProd.thy ex/meson.ML ex/mesontest.ML\
-	   ex/MT.ML ex/MT.thy ex/PL.ML ex/PL.thy ex/Puzzle.ML ex/Puzzle.thy\
+	   ex/MT.ML ex/MT.thy ex/Acc.ML ex/Acc.thy \
+           ex/PL.ML ex/PL.thy ex/Puzzle.ML ex/Puzzle.thy\
            ex/Qsort.thy ex/Qsort.ML\
 	   ex/Rec.ML ex/Rec.thy ex/rel.ML ex/set.ML ex/Simult.ML ex/Simult.thy\
 	   ex/Term.ML ex/Term.thy