--- 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