src/HOL/IsaMakefile
changeset 22784 4637b69de71b
parent 22657 731622340817
child 22799 ed7d53db2170
--- a/src/HOL/IsaMakefile	Tue Apr 24 15:18:42 2007 +0200
+++ b/src/HOL/IsaMakefile	Tue Apr 24 15:19:33 2007 +0200
@@ -98,7 +98,7 @@
   Relation_Power.thy Ring_and_Field.thy SAT.thy Set.thy SetInterval.thy		\
   Sum_Type.thy Tools/res_reconstruct.ML Tools/ATP/reduce_axiomsN.ML	\
   Tools/ATP/watcher.ML Tools/cnf_funcs.ML Tools/datatype_abs_proofs.ML		\
-  Tools/datatype_aux.ML Tools/datatype_codegen.ML				\
+  Tools/datatype_aux.ML Tools/datatype_case.ML Tools/datatype_codegen.ML	\
   Tools/datatype_hooks.ML Tools/datatype_package.ML				\
   Tools/datatype_prop.ML Tools/datatype_realizer.ML				\
   Tools/datatype_rep_proofs.ML Tools/function_package/auto_term.ML		\
@@ -730,6 +730,7 @@
 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML \
   Nominal/Nominal.thy \
   Nominal/nominal_atoms.ML \
+  Nominal/nominal_fresh_fun.ML \
   Nominal/nominal_induct.ML \
   Nominal/nominal_inductive.ML \
   Nominal/nominal_package.ML \