src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
changeset 63352 4eaf35781b23
parent 63285 e9c777bfd78c
child 63391 6840e808fe44
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Thu Jun 23 11:01:14 2016 +0200
@@ -285,7 +285,7 @@
   handle Fail _ => [];
 
 fun set_transfer_rule_attrs thms =
-  snd o Local_Theory.notes [((Binding.empty, []), [(thms, transfer_rule_attrs)])];
+  snd o Local_Theory.notes [(Binding.empty_atts, [(thms, transfer_rule_attrs)])];
 
 fun ensure_codatatype_extra fpT_name ctxt =
   (case codatatype_extra_of ctxt fpT_name of
@@ -1995,7 +1995,7 @@
 
     val (plugins, friend, transfer) = get_options lthy opts;
     val ([((b, fun_T), mx)], [(_, eq)]) =
-      fst (Specification.read_multi_specs raw_fixes [((Attrib.empty_binding, raw_eq), [], [])] lthy);
+      fst (Specification.read_multi_specs raw_fixes [((Binding.empty_atts, raw_eq), [], [])] lthy);
 
     val _ = Sign.of_sort (Proof_Context.theory_of lthy) (fun_T, @{sort type}) orelse
       error ("Type of " ^ Binding.print b ^ " contains top sort");