# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1272429610 -7200
# Node ID b6b3374a402d61db6a826a018fc167fa8e216df6
# Parent  4a3c05fe2bc509cd937d58e9d01f259da4beeabb
factured out common functionality of prefixing the dt-names with a string

diff -r 4a3c05fe2bc5 -r b6b3374a402d Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Wed Apr 28 06:24:10 2010 +0200
+++ b/Nominal/NewFv.thy	Wed Apr 28 06:40:10 2010 +0200
@@ -225,8 +225,7 @@
   val thy = ProofContext.theory_of lthy;
   val {descr, sorts, ...} = dt_info;
 
-  val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
-    "fv_" ^ Datatype_Aux.name_of_typ (nth_dtyp descr sorts i)) descr);
+  val fv_names = prefix_dt_names descr sorts "fv_"
 
   val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
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