put an underscore between names, for compatibility with old package (and also because it makes sense)
authorblanchet
Wed Sep 12 11:38:22 2012 +0200 (2012-09-12)
changeset 49327541d818d2ff3
parent 49326 a063a96c8662
child 49328 a1c10b46fecd
put an underscore between names, for compatibility with old package (and also because it makes sense)
src/HOL/Codatatype/Tools/bnf_fp_util.ML
src/HOL/Codatatype/Tools/bnf_gfp.ML
src/HOL/Codatatype/Tools/bnf_lfp.ML
     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
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 10:36:00 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 11:38:22 2012 +0200
     2.3 @@ -64,7 +64,7 @@
     2.4      val ks = 1 upto n;
     2.5      val m = live - n (*passive, if 0 don't generate a new bnf*);
     2.6      val ls = 1 upto m;
     2.7 -    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
     2.8 +    val b = Binding.name (mk_bundle_name bs);
     2.9  
    2.10      (* TODO: check if m, n etc are sane *)
    2.11  
    2.12 @@ -1675,7 +1675,7 @@
    2.13          map (fn i => map (fn i' =>
    2.14            split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
    2.15              else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
    2.16 -              (2, @{thm sum_case_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
    2.17 +              (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
    2.18                (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
    2.19        end;
    2.20  
     3.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 10:36:00 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 11:38:22 2012 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4      val n = length bnfs; (*active*)
     3.5      val ks = 1 upto n;
     3.6      val m = live - n; (*passive, if 0 don't generate a new bnf*)
     3.7 -    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
     3.8 +    val b = Binding.name (mk_bundle_name bs);
     3.9  
    3.10      (* TODO: check if m, n etc are sane *)
    3.11