# HG changeset patch
# User blanchet
# Date 1370526977 -7200
# Node ID 74315fe137baa0344adf9bf6b01e3170ff040e93
# Parent  30d516bbf19fac7d2c50511108b519a92400d67d
too much qualification is like too little

diff -r 30d516bbf19f -r 74315fe137ba src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Jun 06 15:49:09 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Thu Jun 06 15:56:17 2013 +0200
@@ -207,7 +207,7 @@
     fun is_disc_binding_valid b =
       not (Binding.is_empty b orelse Binding.eq_name (b, equal_binding));
 
-    val standard_disc_binding = qualify false o Binding.name o prefix isN o base_name_of_ctr;
+    val standard_disc_binding = Binding.name o prefix isN o base_name_of_ctr;
 
     val disc_bindings =
       raw_disc_bindings'