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.
qualify map and rel names
authorblanchet
Mon, 12 Aug 2013 09:38:42 +0200
changeset 52964 33dd3795ec22
parent 52963 96754402c851
child 52965 0cd62cb233e0
qualify map and rel names
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 12 09:08:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 12 09:38:42 2013 +0200
@@ -987,8 +987,8 @@
     val fp_bs = map type_binding_of specs;
     val fp_b_names = map Binding.name_of fp_bs;
     val fp_common_name = mk_common_name fp_b_names;
-    val map_bs = map map_binding_of specs;
-    val rel_bs = map rel_binding_of specs;
+    val map_bs = map2 (fn fp_b_name => qualify false fp_b_name o map_binding_of) fp_b_names specs;
+    val rel_bs = map2 (fn fp_b_name => qualify false fp_b_name o rel_binding_of) fp_b_names specs;
 
     fun prepare_type_arg (_, (ty, c)) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
isabelle