# HG changeset patch
# User berghofe
# Date 1164625880 -3600
# Node ID 4462ee172ef07278c3b6e864121c16e72daab2a4
# Parent  ea881fbe0489521914341bde24d159673b9fcdde
Added nominal_primrec.ML

diff -r ea881fbe0489 -r 4462ee172ef0 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Mon Nov 27 12:10:51 2006 +0100
+++ b/src/HOL/IsaMakefile	Mon Nov 27 12:11:20 2006 +0100
@@ -739,7 +739,8 @@
 
 $(OUT)/HOL-Nominal: $(OUT)/HOL Nominal/ROOT.ML Nominal/Nominal.thy		\
   Nominal/nominal_atoms.ML Nominal/nominal_induct.ML				\
-  Nominal/nominal_package.ML Nominal/nominal_permeq.ML Library/Infinite_Set.thy
+  Nominal/nominal_package.ML Nominal/nominal_permeq.ML Nominal/nominal_primrec.ML \
+  Library/Infinite_Set.thy
 	@cd Nominal; $(ISATOOL) usedir -b -g true $(OUT)/HOL HOL-Nominal