# HG changeset patch
# User blanchet
# Date 1376335836 -7200
# Node ID d1bdc6a974605d4b22827e60cc104fc289bbdb67
# Parent  b44a11b87b85d3177f3412e7732ef6ca623898da
avoid double qualification for case constants

diff -r b44a11b87b85 -r d1bdc6a97460 src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Aug 12 21:30:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Aug 12 21:30:36 2013 +0200
@@ -192,8 +192,8 @@
       pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
 
     val Type (dataT_name, As0) = body_type (fastype_of (hd ctrs0));
-    val data_b = Binding.qualified_name dataT_name;
-    val data_b_name = Binding.name_of data_b;
+    val data_b_name = Long_Name.base_name dataT_name;
+    val data_b = Binding.name data_b_name;
 
     fun qualify mandatory =
       Binding.qualify mandatory data_b_name o