src/HOL/Codatatype/Tools/bnf_gfp.ML
changeset 49327 541d818d2ff3
parent 49311 56fcd826f90c
child 49330 276ff43ee0b1
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 10:36:00 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 11:38:22 2012 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4      val ks = 1 upto n;
     1.5      val m = live - n (*passive, if 0 don't generate a new bnf*);
     1.6      val ls = 1 upto m;
     1.7 -    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
     1.8 +    val b = Binding.name (mk_bundle_name bs);
     1.9  
    1.10      (* TODO: check if m, n etc are sane *)
    1.11  
    1.12 @@ -1675,7 +1675,7 @@
    1.13          map (fn i => map (fn i' =>
    1.14            split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
    1.15              else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
    1.16 -              (2, @{thm sum_case_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
    1.17 +              (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
    1.18                (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
    1.19        end;
    1.20