src/HOL/BNF/Tools/bnf_ctr_sugar.ML

       Binding.qualify mandatory data_b_name o
       (rep_compat ? Binding.qualify false rep_compat_prefix);
 
     val (As, B) =
       no_defs_lthy
-      |> variant_tfrees (map (fst o fst o dest_TVar) As0)
+      |> variant_tfrees (map base_name_of_typ As0)
       ||> the_single o fst o mk_TFrees 1;
 
     val dataT = Type (dataT_name, As);
     val ctrs = map (mk_ctr As) ctrs0;
     val ctr_Tss = map (binder_types o fastype_of) ctrs;