# HG changeset patch
# User blanchet
# Date 1376293122 -7200
# Node ID 33dd3795ec22835b173d79b3403e69c3a9db4748
# Parent  96754402c85155ca87b394a56b2f464865fd89f4
qualify map and rel names

diff -r 96754402c851 -r 33dd3795ec22 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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