# HG changeset patch
# User berghofe
# Date 1177420773 -7200
# Node ID 4637b69de71bcfec4e514e2babd0f74efcf1d1d1
# Parent  e5f947e0ade8f59a2333a48b5b3ed72967228913
Added datatype_case.ML and nominal_fresh_fun.ML.

diff -r e5f947e0ade8 -r 4637b69de71b src/HOL/IsaMakefile
--- 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 \