src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML

--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Wed Jun 22 16:04:03 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Thu Jun 23 11:01:14 2016 +0200
@@ -1609,7 +1609,7 @@
    || Parse.reserved "transfer" >> K Transfer_Option);
 
 val where_alt_props_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
-  ((Parse.prop >> pair Attrib.empty_binding) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
+  ((Parse.prop >> pair Binding.empty_atts) -- Scan.option (Parse.reserved "of" |-- Parse.const)));
 
 val _ = Outer_Syntax.local_theory_to_proof @{command_keyword primcorecursive}
   "define primitive corecursive functions"