# HG changeset patch
# User blanchet
# Date 1377786371 -7200
# Node ID 1973b821168cd47635e3ee4f5a670dc15a067959
# Parent  d4784d3d3a54bd7aa1fbf970df436eca6cc2fce5
qualify generated constants uniformly

diff -r d4784d3d3a54 -r 1973b821168c src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 15:02:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Thu Aug 29 16:26:11 2013 +0200
@@ -24,8 +24,8 @@
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
     (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
     (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
-  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
-    (BNF_Def.bnf * typ list) * local_theory
+  val seal_bnf: (binding -> binding) -> unfold_set -> binding -> typ list -> BNF_Def.bnf ->
+    Proof.context -> (BNF_Def.bnf * typ list) * local_theory
 end;
 
 structure BNF_Comp : BNF_COMP =
@@ -434,7 +434,6 @@
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Dont_Note) qualify tacs wit_tac (SOME Ds) Binding.empty Binding.empty
         [] (((((b, mapx), sets), Term.absdummy T bd), wits), SOME rel) lthy;
-
   in
     (bnf', (add_bnf_to_unfolds bnf' unfold_set, lthy'))
   end;
@@ -571,7 +570,7 @@
 
 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
 
-fun seal_bnf (unfold_set : unfold_set) b Ds bnf lthy =
+fun seal_bnf qualify (unfold_set : unfold_set) b Ds bnf lthy =
   let
     val live = live_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
@@ -604,7 +603,7 @@
 
     (*bd should only depend on dead type variables!*)
     val bd_repT = fst (dest_relT (fastype_of bnf_bd));
-    val bdT_bind = Binding.suffix_name ("_" ^ bdTN) b;
+    val bdT_bind = qualify (Binding.suffix_name ("_" ^ bdTN) b);
     val params = fold Term.add_tfreesT Ds [];
     val deads = map TFree params;
 
@@ -641,9 +640,10 @@
 
     fun wit_tac _ = mk_simple_wit_tac (map unfold_all (wit_thms_of_bnf bnf));
 
-    val (bnf', lthy') = bnf_def Hardly_Inline (user_policy Dont_Note) I tacs wit_tac (SOME deads)
-      Binding.empty Binding.empty []
-      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
+    val (bnf', lthy') =
+      bnf_def Hardly_Inline (user_policy Dont_Note) qualify tacs wit_tac (SOME deads)
+        Binding.empty Binding.empty []
+        (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), SOME bnf_rel) lthy;
   in
     ((bnf', deads), lthy')
   end;
diff -r d4784d3d3a54 -r 1973b821168c src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 15:02:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 29 16:26:11 2013 +0200
@@ -1034,8 +1034,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 = 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;
+    val map_bs = map map_binding_of specs;
+    val rel_bs = map rel_binding_of specs;
 
     fun prepare_type_arg (_, (ty, c)) =
       let val TFree (s, _) = prepare_typ no_defs_lthy0 ty in
diff -r d4784d3d3a54 -r 1973b821168c src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 15:02:42 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 29 16:26:11 2013 +0200
@@ -582,19 +582,18 @@
     fun fp_sort Ass =
       subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
 
-    val common_name = mk_common_name (map Binding.name_of bs);
-
     fun raw_qualify base_b =
-      Binding.prefix_name rawN
-      #> fold_rev (fn (s, mand) => Binding.qualify mand s) (#2 (Binding.dest base_b));
+      let val (_, qs, n) = Binding.dest base_b;
+      in
+        Binding.prefix_name rawN
+        #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
+      end;
 
     val ((bnfs, (deadss, livess)), (unfold_set, lthy)) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (raw_qualify b) fp_sort Xs) bs rhsXs
         (empty_unfolds, lthy));
 
-    fun qualify i =
-      let val namei = common_name ^ nonzero_string_of_int i;
-      in Binding.qualify true namei end;
+    fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))));
 
     val Ass = map (map dest_TFree) livess;
     val resDs = fold (subtract (op =)) Ass resBs;
@@ -603,12 +602,15 @@
     val timer = time (timer "Construction of BNFs");
 
     val ((kill_poss, _), (bnfs', (unfold_set', lthy'))) =
-      normalize_bnfs qualify Ass Ds fp_sort bnfs unfold_set lthy;
+      normalize_bnfs norm_qualify Ass Ds fp_sort bnfs unfold_set lthy;
 
     val Dss = map3 (append oo map o nth) livess kill_poss deadss;
 
+    val pre_qualify = Binding.qualify false o Binding.name_of;
+
     val ((pre_bnfs, deadss), lthy'') =
-      fold_map3 (seal_bnf unfold_set') (map (Binding.prefix_name preN) bs) Dss bnfs' lthy'
+      fold_map3 (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
+        bs Dss bnfs' lthy'
       |>> split_list;
 
     val timer = time (timer "Normalization & sealing of BNFs");