# HG changeset patch
# User wenzelm
# Date 1460982381 -7200
# Node ID 3c2df99b7b1dbac1036764ca26de6257188a548d
# Parent  b577a13a15f3656b90be069575e4705a678a4211
tuned;

diff -r b577a13a15f3 -r 3c2df99b7b1d src/HOL/Tools/BNF/bnf_def.ML
--- 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