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