--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Jun 23 11:01:14 2016 +0200
@@ -133,7 +133,7 @@
(* 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 *)
@@ -143,7 +143,7 @@
:: 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 *)
@@ -251,7 +251,7 @@
@ (#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 =