diff -r 4a3c05fe2bc5 -r b6b3374a402d Nominal/Perm.thy
--- a/Nominal/Perm.thy	Wed Apr 28 06:24:10 2010 +0200
+++ b/Nominal/Perm.thy	Wed Apr 28 06:40:10 2010 +0200
@@ -12,6 +12,19 @@
 *}
 
 ML {*
+(* generates for every datatype a name str ^ dt_name *)
+fun prefix_dt_names dt_descr sorts str = 
+let
+  fun get_nth_name (i, _) = 
+    Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i) 
+in
+  Datatype_Prop.indexify_names 
+    (map (prefix str o get_nth_name) dt_descr)
+end
+*}
+
+
+ML {*
 (* permutation function for one argument 
    
     - in case the argument is recursive it returns 
@@ -108,8 +121,7 @@
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
   val full_tnames = List.take (all_full_tnames, dt_nos);
 
-  val perm_fn_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
-    "permute_" ^ Datatype_Aux.name_of_typ (nth_dtyp dt_descr sorts i)) dt_descr);
+  val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
 
   val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr