cleaned up internal naming scheme for bnfs

--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Mon Sep 17 15:38:16 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Mon Sep 17 16:57:22 2012 +0200
@@ -15,7 +15,7 @@
   val rel_unfolds_of: unfold_thms -> thm list
   val pred_unfolds_of: unfold_thms -> thm list
 
-  val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
+  val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
     (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
   val default_comp_sort: (string * sort) list list -> (string * sort) list
@@ -68,10 +68,10 @@
 
 val bdTN = "bdT";
 
-fun mk_killN n = "kill" ^ string_of_int n ^ "_";
-fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
+fun mk_killN n = "_kill" ^ string_of_int n;
+fun mk_liftN n = "_lift" ^ string_of_int n;
 fun mk_permuteN src dest =
-  "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_";
+  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
 val no_thm = refl;
 val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
@@ -286,7 +286,7 @@
 
 fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   let
-    val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
+    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
     val dead = dead_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
@@ -385,7 +385,7 @@
 
 fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
   let
-    val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
+    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
     val dead = dead_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
@@ -474,7 +474,7 @@
 
 fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
   let
-    val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
+    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
     val live = live_of_bnf bnf;
     val dead = dead_of_bnf bnf;
     val nwits = nwits_of_bnf bnf;
@@ -590,15 +590,9 @@
 fun default_comp_sort Ass =
   Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
 
-fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
+fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
   let
-    val name = Binding.name_of b;
-    fun qualify i bind =
-      let val namei = if i > 0 then name ^ string_of_int i else name;
-      in
-        if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
-        else qualify' (Binding.prefix_name namei bind)
-      end;
+    val b = name_of_bnf outer;
 
     val Ass = map (map Term.dest_TFree) tfreess;
     val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
@@ -609,7 +603,8 @@
     val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
     val As = map TFree As;
   in
-    apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
+    apfst (rpair (Ds, As))
+      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
   end;
 
 (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
@@ -707,11 +702,11 @@
     ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
   end;
 
-fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
+fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
     ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
       (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
-  | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
-  | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
+  | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
+  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     let
       val tfrees = Term.add_tfreesT T [];
       val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
@@ -734,13 +729,10 @@
           in ((bnf, deads_lives), (unfold', lthy)) end
         else
           let
-            val name = Binding.name_of b;
-            fun qualify i bind =
-              let val namei = if i > 0 then name ^ string_of_int i else name;
-              in
-                if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
-                else qualify' (Binding.prefix_name namei bind)
-              end;
+            val name = Long_Name.base_name C;
+            fun qualify i =
+              let val namei = name ^ nonzero_string_of_int i;
+              in qualify' o Binding.qualify true namei end;
             val odead = dead_of_bnf bnf;
             val olive = live_of_bnf bnf;
             val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
@@ -749,11 +741,10 @@
             val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
             val ((inners, (Dss, Ass)), (unfold', lthy')) =
               apfst (apsnd split_list o split_list)
-                (fold_map2 (fn i =>
-                  bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
+                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
                 (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
           in
-            compose_bnf const_policy (qualify 0) b sort bnf inners oDs Dss Ass (unfold', lthy')
+            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')
           end)
     end;
 

--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 15:38:16 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 16:57:22 2012 +0200
@@ -461,9 +461,6 @@
 
 (* Names *)
 
-fun nonzero_string_of_int 0 = ""
-  | nonzero_string_of_int n = string_of_int n;
-
 val mapN = "map";
 val setN = "set";
 fun mk_setN i = setN ^ nonzero_string_of_int i;
@@ -536,6 +533,8 @@
     val live = length raw_sets;
     val nwits = length raw_wits;
 
+    val _ = tracing (Binding.name_of b)
+
     val map_rhs = prep_term no_defs_lthy raw_map;
     val set_rhss = map (prep_term no_defs_lthy) raw_sets;
     val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 17 15:38:16 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 17 16:57:22 2012 +0200
@@ -375,12 +375,9 @@
 fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
   let
     val name = mk_common_name bs;
-    fun qualify i bind =
-      let val namei = if i > 0 then name ^ string_of_int i else name;
-      in
-        if member (op =) (#2 (Binding.dest bind)) (namei, true) then bind
-        else Binding.prefix_name namei bind
-      end;
+    fun qualify i =
+      let val namei = name ^ nonzero_string_of_int i;
+      in Binding.qualify true namei end;
 
     val Ass = map (map dest_TFree) livess;
     val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
@@ -415,8 +412,9 @@
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
     val sort = fp_sort lhss (SOME resBs);
+    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
-      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort) bs rhss
+      (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfold, lthy));
   in
     mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
@@ -427,9 +425,10 @@
     val timer = time (Timer.startRealTimer ());
     val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
     val sort = fp_sort lhss NONE;
+    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
     val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
       (fold_map2 (fn b => fn rawT =>
-        (bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort (Syntax.read_typ lthy rawT)))
+        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
       bs raw_bnfs (empty_unfold, lthy));
   in
     snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')

--- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 15:38:16 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 16:57:22 2012 +0200
@@ -58,6 +58,7 @@
     (term list * (string * typ) list) * Proof.context
   val mk_Freess': string -> typ list list -> Proof.context ->
     (term list list * (string * typ) list list) * Proof.context
+  val nonzero_string_of_int: int -> string
 
   val strip_typeN: int -> typ -> typ list * typ
 
@@ -286,6 +287,9 @@
 
 (** Fresh variables **)
 
+fun nonzero_string_of_int 0 = ""
+  | nonzero_string_of_int n = string_of_int n;
+
 val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
 
 fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);