src/HOL/Tools/Transfer/transfer_bnf.ML

 
 fun prove_relation_constraints bnf lthy =
   let
     val transfer_attr = @{attributes [transfer_rule]}
     val Tname = base_name_of_bnf bnf
-    fun qualify suffix = Binding.qualified true suffix Tname
 
     val defs = map (apsnd (prove_relation_side_constraint lthy bnf)) defs
     val bi_total = prove_relation_bi_constraint lthy bnf @{thm bi_total_alt_def}
       [snd (nth defs 0), snd (nth defs 1)]
     val bi_unique = prove_relation_bi_constraint lthy bnf @{thm bi_unique_alt_def}
       [snd (nth defs 2), snd (nth defs 3)]
     val defs = ("bi_total_rel", bi_total) :: ("bi_unique_rel", bi_unique) :: defs
-    val notes = maps (fn (name, thm) => [((qualify name, []), [([thm], transfer_attr)])]) defs
-  in
-    notes
+  in
+    maps (fn (a, thm) => [((Binding.qualify_name true Tname a, []), [([thm], transfer_attr)])]) defs
   end
 
 (* relator_eq *)
 
 fun relator_eq bnf =

 fun predicator bnf lthy =
   let
     val pred_def = pred_set_of_bnf bnf
     val Domainp_rel = prove_Domainp_rel lthy bnf pred_def
     val rel_eq_onp = rel_eq_onp_of_bnf bnf
-    fun qualify defname suffix = Binding.qualified true suffix defname
-    val Domainp_rel_thm_name = qualify (base_name_of_bnf bnf) "Domainp_rel"
+    val Domainp_rel_thm_name = Binding.qualify_name true (base_name_of_bnf bnf) "Domainp_rel"
     val pred_data = Transfer.mk_pred_data pred_def rel_eq_onp []
     val type_name = type_name_of_bnf bnf
     val relator_domain_attr = @{attributes [relator_domain]}
     val notes = [((Domainp_rel_thm_name, []), [([Domainp_rel], relator_domain_attr)])]
   in