src/HOL/Codatatype/Tools/bnf_fp_util.ML
changeset 49327 541d818d2ff3
parent 49308 6190b701e4f4
child 49330 276ff43ee0b1
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 10:36:00 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 11:38:22 2012 +0200
     1.3 @@ -78,6 +78,8 @@
     1.4    val mk_set_minimalN: int -> string
     1.5    val mk_set_inductN: int -> string
     1.6  
     1.7 +  val mk_bundle_name: binding list -> string
     1.8 +
     1.9    val split_conj_thm: thm -> thm list
    1.10    val split_conj_prems: int -> thm -> thm
    1.11  
    1.12 @@ -207,6 +209,8 @@
    1.13  val set_inclN = "set_incl"
    1.14  val set_set_inclN = "set_set_incl"
    1.15  
    1.16 +val mk_bundle_name = space_implode "_" o map Binding.name_of;
    1.17 +
    1.18  fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
    1.19  
    1.20  fun dest_sumTN 1 T = [T]
    1.21 @@ -319,7 +323,7 @@
    1.22  
    1.23  fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
    1.24    let
    1.25 -    val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
    1.26 +    val name = mk_bundle_name bs;
    1.27      fun qualify i bind =
    1.28        let val namei = if i > 0 then name ^ string_of_int i else name;
    1.29        in