1.1 --- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Mon Sep 17 15:38:16 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Mon Sep 17 16:57:22 2012 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    val rel_unfolds_of: unfold_thms -> thm list
     1.5    val pred_unfolds_of: unfold_thms -> thm list
     1.6  
     1.7 -  val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
     1.8 +  val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     1.9      ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
    1.10      (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
    1.11    val default_comp_sort: (string * sort) list list -> (string * sort) list
    1.12 @@ -68,10 +68,10 @@
    1.13  
    1.14  val bdTN = "bdT";
    1.15  
    1.16 -fun mk_killN n = "kill" ^ string_of_int n ^ "_";
    1.17 -fun mk_liftN n = "lift" ^ string_of_int n ^ "_";
    1.18 +fun mk_killN n = "_kill" ^ string_of_int n;
    1.19 +fun mk_liftN n = "_lift" ^ string_of_int n;
    1.20  fun mk_permuteN src dest =
    1.21 -  "permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest) ^ "_";
    1.22 +  "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
    1.23  
    1.24  val no_thm = refl;
    1.25  val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
    1.26 @@ -286,7 +286,7 @@
    1.27  
    1.28  fun kill_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
    1.29    let
    1.30 -    val b = Binding.prefix_name (mk_killN n) (name_of_bnf bnf);
    1.31 +    val b = Binding.suffix_name (mk_killN n) (name_of_bnf bnf);
    1.32      val live = live_of_bnf bnf;
    1.33      val dead = dead_of_bnf bnf;
    1.34      val nwits = nwits_of_bnf bnf;
    1.35 @@ -385,7 +385,7 @@
    1.36  
    1.37  fun lift_bnf qualify n bnf (unfold, lthy) = if n = 0 then (bnf, (unfold, lthy)) else
    1.38    let
    1.39 -    val b = Binding.prefix_name (mk_liftN n) (name_of_bnf bnf);
    1.40 +    val b = Binding.suffix_name (mk_liftN n) (name_of_bnf bnf);
    1.41      val live = live_of_bnf bnf;
    1.42      val dead = dead_of_bnf bnf;
    1.43      val nwits = nwits_of_bnf bnf;
    1.44 @@ -474,7 +474,7 @@
    1.45  
    1.46  fun permute_bnf qualify src dest bnf (unfold, lthy) = if src = dest then (bnf, (unfold, lthy)) else
    1.47    let
    1.48 -    val b = Binding.prefix_name (mk_permuteN src dest) (name_of_bnf bnf);
    1.49 +    val b = Binding.suffix_name (mk_permuteN src dest) (name_of_bnf bnf);
    1.50      val live = live_of_bnf bnf;
    1.51      val dead = dead_of_bnf bnf;
    1.52      val nwits = nwits_of_bnf bnf;
    1.53 @@ -590,15 +590,9 @@
    1.54  fun default_comp_sort Ass =
    1.55    Library.sort (Term_Ord.typ_ord o pairself TFree) (fold (fold (insert (op =))) Ass []);
    1.56  
    1.57 -fun compose_bnf const_policy qualify' b sort outer inners oDs Dss tfreess (unfold, lthy) =
    1.58 +fun compose_bnf const_policy qualify sort outer inners oDs Dss tfreess (unfold, lthy) =
    1.59    let
    1.60 -    val name = Binding.name_of b;
    1.61 -    fun qualify i bind =
    1.62 -      let val namei = if i > 0 then name ^ string_of_int i else name;
    1.63 -      in
    1.64 -        if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
    1.65 -        else qualify' (Binding.prefix_name namei bind)
    1.66 -      end;
    1.67 +    val b = name_of_bnf outer;
    1.68  
    1.69      val Ass = map (map Term.dest_TFree) tfreess;
    1.70      val Ds = fold (fold Term.add_tfreesT) (oDs :: Dss) [];
    1.71 @@ -609,7 +603,8 @@
    1.72      val Ds = oDs @ flat (map3 (append oo map o nth) tfreess kill_poss Dss);
    1.73      val As = map TFree As;
    1.74    in
    1.75 -    apfst (rpair (Ds, As)) (clean_compose_bnf const_policy I b outer inners' (unfold', lthy'))
    1.76 +    apfst (rpair (Ds, As))
    1.77 +      (clean_compose_bnf const_policy (qualify 0) b outer inners' (unfold', lthy'))
    1.78    end;
    1.79  
    1.80  (* Hide the type of the bound (optimization) and unfold the definitions (nicer to the user) *)
    1.81 @@ -707,11 +702,11 @@
    1.82      ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
    1.83    end;
    1.84  
    1.85 -fun bnf_of_typ _ _ _ _ (T as TFree _) (unfold, lthy) =
    1.86 +fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
    1.87      ((Basic_BNFs.ID_bnf, ([], [T])), (add_to_unfold_opt NONE NONE
    1.88        (SOME Basic_BNFs.ID_rel_def) (SOME Basic_BNFs.ID_pred_def) unfold, lthy))
    1.89 -  | bnf_of_typ _ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
    1.90 -  | bnf_of_typ const_policy b qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
    1.91 +  | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
    1.92 +  | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
    1.93      let
    1.94        val tfrees = Term.add_tfreesT T [];
    1.95        val bnf_opt = if null tfrees then NONE else bnf_of lthy C;
    1.96 @@ -734,13 +729,10 @@
    1.97            in ((bnf, deads_lives), (unfold', lthy)) end
    1.98          else
    1.99            let
   1.100 -            val name = Binding.name_of b;
   1.101 -            fun qualify i bind =
   1.102 -              let val namei = if i > 0 then name ^ string_of_int i else name;
   1.103 -              in
   1.104 -                if member (op =) (#2 (Binding.dest bind)) (namei, true) then qualify' bind
   1.105 -                else qualify' (Binding.prefix_name namei bind)
   1.106 -              end;
   1.107 +            val name = Long_Name.base_name C;
   1.108 +            fun qualify i =
   1.109 +              let val namei = name ^ nonzero_string_of_int i;
   1.110 +              in qualify' o Binding.qualify true namei end;
   1.111              val odead = dead_of_bnf bnf;
   1.112              val olive = live_of_bnf bnf;
   1.113              val oDs_pos = find_indices [TFree ("dead", [])] (snd (Term.dest_Type
   1.114 @@ -749,11 +741,10 @@
   1.115              val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
   1.116              val ((inners, (Dss, Ass)), (unfold', lthy')) =
   1.117                apfst (apsnd split_list o split_list)
   1.118 -                (fold_map2 (fn i =>
   1.119 -                  bnf_of_typ Smart_Inline (Binding.name (name ^ string_of_int i)) (qualify i) sort)
   1.120 +                (fold_map2 (fn i => bnf_of_typ Smart_Inline (qualify i) sort)
   1.121                  (if length Ts' = 1 then [0] else (1 upto length Ts')) Ts' (unfold, lthy));
   1.122            in
   1.123 -            compose_bnf const_policy (qualify 0) b sort bnf inners oDs Dss Ass (unfold', lthy')
   1.124 +            compose_bnf const_policy qualify sort bnf inners oDs Dss Ass (unfold', lthy')
   1.125            end)
   1.126      end;
   1.127  

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 15:38:16 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Mon Sep 17 16:57:22 2012 +0200
     2.3 @@ -461,9 +461,6 @@
     2.4  
     2.5  (* Names *)
     2.6  
     2.7 -fun nonzero_string_of_int 0 = ""
     2.8 -  | nonzero_string_of_int n = string_of_int n;
     2.9 -
    2.10  val mapN = "map";
    2.11  val setN = "set";
    2.12  fun mk_setN i = setN ^ nonzero_string_of_int i;
    2.13 @@ -536,6 +533,8 @@
    2.14      val live = length raw_sets;
    2.15      val nwits = length raw_wits;
    2.16  
    2.17 +    val _ = tracing (Binding.name_of b)
    2.18 +
    2.19      val map_rhs = prep_term no_defs_lthy raw_map;
    2.20      val set_rhss = map (prep_term no_defs_lthy) raw_sets;
    2.21      val (bd_rhsT, bd_rhs) = (case prep_term no_defs_lthy raw_bd_Abs of

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 17 15:38:16 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Mon Sep 17 16:57:22 2012 +0200
     3.3 @@ -375,12 +375,9 @@
     3.4  fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
     3.5    let
     3.6      val name = mk_common_name bs;
     3.7 -    fun qualify i bind =
     3.8 -      let val namei = if i > 0 then name ^ string_of_int i else name;
     3.9 -      in
    3.10 -        if member (op =) (#2 (Binding.dest bind)) (namei, true) then bind
    3.11 -        else Binding.prefix_name namei bind
    3.12 -      end;
    3.13 +    fun qualify i =
    3.14 +      let val namei = name ^ nonzero_string_of_int i;
    3.15 +      in Binding.qualify true namei end;
    3.16  
    3.17      val Ass = map (map dest_TFree) livess;
    3.18      val resDs = (case resBs of NONE => [] | SOME Ts => fold (subtract (op =)) Ass Ts);
    3.19 @@ -415,8 +412,9 @@
    3.20      val timer = time (Timer.startRealTimer ());
    3.21      val (lhss, rhss) = split_list eqs;
    3.22      val sort = fp_sort lhss (SOME resBs);
    3.23 +    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
    3.24      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    3.25 -      (fold_map2 (fn b => bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort) bs rhss
    3.26 +      (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
    3.27          (empty_unfold, lthy));
    3.28    in
    3.29      mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold lthy'
    3.30 @@ -427,9 +425,10 @@
    3.31      val timer = time (Timer.startRealTimer ());
    3.32      val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
    3.33      val sort = fp_sort lhss NONE;
    3.34 +    fun qualify b = Binding.qualify true (Binding.name_of (Binding.prefix_name rawN b));
    3.35      val ((bnfs, (Dss, Ass)), (unfold, lthy')) = apfst (apsnd split_list o split_list)
    3.36        (fold_map2 (fn b => fn rawT =>
    3.37 -        (bnf_of_typ Smart_Inline (Binding.prefix_name rawN b) I sort (Syntax.read_typ lthy rawT)))
    3.38 +        (bnf_of_typ Smart_Inline (qualify b) sort (Syntax.read_typ lthy rawT)))
    3.39        bs raw_bnfs (empty_unfold, lthy));
    3.40    in
    3.41      snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 15:38:16 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_util.ML	Mon Sep 17 16:57:22 2012 +0200
     4.3 @@ -58,6 +58,7 @@
     4.4      (term list * (string * typ) list) * Proof.context
     4.5    val mk_Freess': string -> typ list list -> Proof.context ->
     4.6      (term list list * (string * typ) list list) * Proof.context
     4.7 +  val nonzero_string_of_int: int -> string
     4.8  
     4.9    val strip_typeN: int -> typ -> typ list * typ
    4.10  
    4.11 @@ -286,6 +287,9 @@
    4.12  
    4.13  (** Fresh variables **)
    4.14  
    4.15 +fun nonzero_string_of_int 0 = ""
    4.16 +  | nonzero_string_of_int n = string_of_int n;
    4.17 +
    4.18  val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
    4.19  
    4.20  fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);