Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
conceal even more ugly constructions
authorblanchet
Fri, 18 Oct 2013 15:42:55 +0200
changeset 54156 a8cf84bfa9be
parent 54155 b964fad0cbbd
child 54157 5874be04e1f9
conceal even more ugly constructions
src/HOL/BNF/Tools/bnf_def.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 15:25:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Oct 18 15:42:55 2013 +0200
@@ -633,7 +633,7 @@
         | T => err T)
       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
 
-    val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
+    val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
 
     fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
isabelle