diff -r ce378dcfddab -r abe0f11cfa4e src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:42:39 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:43:42 2008 +0100
@@ -230,7 +230,7 @@
 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
   let
     val (raw_eqns, atts) = split_list eqns_atts;
-    val eqns = map (apfst Name.name_of) raw_eqns;
+    val eqns = map (apfst Binding.base_name) raw_eqns;
     val dt_info = NominalPackage.get_nominal_datatypes thy;
     val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>