diff -r e05c620eceeb -r aa8cf5eed06e src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Oct 30 09:15:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Oct 30 11:08:26 2014 +0100
@@ -127,7 +127,7 @@
   @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
   Scan.succeed [];
 
-val parse_map_rel_binding = Parse.short_ident --| @{keyword ":"} -- Parse.binding;
+val parse_map_rel_binding = Parse.name --| @{keyword ":"} -- Parse.binding;
 
 val no_map_rel = (Binding.empty, Binding.empty);