--- a/Paper/Paper.thy	Thu Apr 01 06:04:43 2010 +0200
+++ b/Paper/Paper.thy	Thu Apr 01 06:47:37 2010 +0200
@@ -1803,15 +1803,27 @@
   \href{http://isabelle.in.tum.de/nominal/download}
   {http://isabelle.in.tum.de/nominal/download}.
 
+  We have left out a discussion about how functions can be defined
+  over alpha-equated terms. In earlier work \cite{UrbanBerghofer06}
+  this turned out to be a thorny issue in the old Nominal Isabelle.
+  We hope to do better this time by using the function package that
+  has recently been implemented in Isabelle/HOL and by restricting
+  function definitions to equivariant functions (for such functions
+  it is possible to provide more automation).
 
+  There are some restrictions we imposed, like absence of nested type
+  definitions that allow one to specify the function kinds as 
+  @{text "TFun string (ty list)"} instead of the unfolded version
+  @{text "TFun string ty_list"} in Figure~\ref{nominalcorehas}, that 
+  can be easily lifted. They essentially amount only to a more
+  clever implementation. More interesting is lifting our restriction
+  about overlapping deep binders.
+  
   Complication when the single scopedness restriction is lifted (two 
   overlapping permutations)
 
   Future work: distinct list abstraction
 
-  TODO: function definitions:
-  
-  
   \noindent
   {\bf Acknowledgements:} We are very grateful to Andrew Pitts for  
   many discussions about Nominal Isabelle. We thank Peter Sewell for 

--- a/Paper/document/root.bib	Thu Apr 01 06:04:43 2010 +0200
+++ b/Paper/document/root.bib	Thu Apr 01 06:47:37 2010 +0200
@@ -1,3 +1,13 @@
+@InProceedings{ UrbanBerghofer06,
+	author = "C. Urban and S. Berghofer",
+	title = "{A} {R}ecursion {C}ombinator for {N}ominal {D}atatypes {I}mplemented in {I}sabelle/{HOL}",
+	booktitle = "Proc.~of the 3rd IJCAR Conference",
+	year = 2006,
+	series = "LNAI",
+	volume = 4130,
+	pages = "498--512"
+}
+
 @InProceedings{LeeCraryHarper07,
   author = 	 {D.~K.~Lee and K.~Crary and R.~Harper},
   title = 	 {{T}owards a {M}echanized {M}etatheory of {Standard ML}},