diff -r efacb9b99865 -r 5f1dec4297da src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 13:52:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Apr 29 14:06:37 2013 +0200
@@ -75,11 +75,10 @@
     in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
 
 fun add_components_of_typ (Type (s, Ts)) =
-    fold add_components_of_typ Ts
-    #> cons s
+    fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
   | add_components_of_typ _ = I;
 
-fun name_of_typ T = space_implode "_" (add_components_of_typ T []);
+fun base_name_of_typ T = space_implode "_" (add_components_of_typ T []);
 
 fun exists_subtype_in Ts = exists_subtype (member (op =) Ts);
 
@@ -211,12 +210,12 @@
     val nested_set_map's = maps set_map'_of_bnf nested_bnfs;
     val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
 
-    val fp_T_names = map name_of_typ fpTs;
+    val fp_b_names = map base_name_of_typ fpTs;
 
     val (((ps, ps'), us'), names_lthy) =
       lthy
       |> mk_Frees' "P" (map mk_pred1T fpTs)
-      ||>> Variable.variant_fixes fp_T_names;
+      ||>> Variable.variant_fixes fp_b_names;
 
     val us = map2 (curry Free) us' fpTs;
 
@@ -368,7 +367,7 @@
     val nesting_map_ids'' = map (unfold_thms lthy @{thms id_def} o map_id_of_bnf) nesting_bnfs;
     val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
 
-    val fp_T_names = map name_of_typ fpTs;
+    val fp_b_names = map base_name_of_typ fpTs;
 
     val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress;
     val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress;
@@ -380,8 +379,8 @@
     val (((rs, us'), vs'), names_lthy) =
       lthy
       |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
-      ||>> Variable.variant_fixes fp_T_names
-      ||>> Variable.variant_fixes (map (suffix "'") fp_T_names);
+      ||>> Variable.variant_fixes fp_b_names
+      ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
 
     val us = map2 (curry Free) us' fpTs;
     val udiscss = map2 (map o rapp) us discss;
@@ -466,7 +465,7 @@
         flat (map2 append disc_concls ctr_concls)
       end;
 
-    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_T_names);
+    val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
     val coinduct_conclss =
       map3 (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;