Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_ctr_sugar.ML
changeset 52988 d1bdc6a97460
parent 52969 f2df0730f8ac
child 53039 476db75906ae 
--- 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
isabelle