avoid double qualification for case constants
authorblanchet
Mon, 12 Aug 2013 21:30:36 +0200
changeset 52988 d1bdc6a97460
parent 52987 b44a11b87b85
child 52989 729ed0c46e18
avoid double qualification for case constants
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