src/HOL/Tools/Transfer/transfer_bnf.ML

   end
 
 (* relator_eq *)
 
 fun relator_eq bnf =
-  [((Binding.empty, []), [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
+  [(Binding.empty_atts, [([rel_eq_of_bnf bnf], @{attributes [relator_eq]})])]
 
 (* transfer rules *)
 
 fun bnf_transfer_rules bnf =
   let
     val transfer_rules = map_transfer_of_bnf bnf :: pred_transfer_of_bnf bnf
       :: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf
     val transfer_attr = @{attributes [transfer_rule]}
   in
-    map (fn thm => ((Binding.empty,[]),[([thm],transfer_attr)])) transfer_rules
+    map (fn thm => (Binding.empty_atts, [([thm],transfer_attr)])) transfer_rules
   end
 
 (* Domainp theorem for predicator *)
 
 fun Domainp_tac bnf pred_def ctxt =

     val transfer_rules = #ctr_transfers fp_ctr_sugar @ #case_transfers fp_ctr_sugar
       @ #disc_transfers fp_ctr_sugar @ #sel_transfers fp_ctr_sugar
       @ (#co_rec_transfers o #fp_co_induct_sugar) fp_sugar
     val transfer_attr = @{attributes [transfer_rule]}
   in
-    map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules
+    map (fn thm => (Binding.empty_atts, [([thm], transfer_attr)])) transfer_rules
   end
 
 fun register_pred_injects fp_sugar lthy =
   let
     val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar)