tuned;

--- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 18 11:02:07 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Apr 18 14:26:21 2016 +0200
@@ -1187,7 +1187,7 @@
         " as unnamed BNF");
 
     val (bnf_b, key) =
-      if Binding.eq_name (bnf_b, Binding.empty) then
+      if Binding.is_empty bnf_b then
         (case T_rhs of
           Type (C, Ts) => if forall (can dest_TFree) Ts
             then (Binding.qualified_name C, C) else err T_rhs