--- a/Nominal/Perm.thy	Wed Apr 28 07:27:28 2010 +0200
+++ b/Nominal/Perm.thy	Wed Apr 28 08:22:20 2010 +0200
@@ -12,7 +12,8 @@
 *}
 
 ML {*
-(* generates for every datatype a name str ^ dt_name *)
+(* generates for every datatype a name str ^ dt_name 
+   plus and index for multiple occurences of a string *)
 fun prefix_dt_names dt_descr sorts str = 
 let
   fun get_nth_name (i, _) =