# HG changeset patch
# User blanchet
# Date 1347442702 -7200
# Node ID 541d818d2ff3846087f08c6f6813445b52d54d66
# Parent  a063a96c866206640bae2c997becdcbbaa55bd18
put an underscore between names, for compatibility with old package (and also because it makes sense)

diff -r a063a96c8662 -r 541d818d2ff3 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 10:36:00 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Wed Sep 12 11:38:22 2012 +0200
@@ -78,6 +78,8 @@
   val mk_set_minimalN: int -> string
   val mk_set_inductN: int -> string
 
+  val mk_bundle_name: binding list -> string
+
   val split_conj_thm: thm -> thm list
   val split_conj_prems: int -> thm -> thm
 
@@ -207,6 +209,8 @@
 val set_inclN = "set_incl"
 val set_set_inclN = "set_set_incl"
 
+val mk_bundle_name = space_implode "_" o map Binding.name_of;
+
 fun dest_sumT (Type (@{type_name sum}, [T, T'])) = (T, T');
 
 fun dest_sumTN 1 T = [T]
@@ -319,7 +323,7 @@
 
 fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold lthy =
   let
-    val name = fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "";
+    val name = mk_bundle_name bs;
     fun qualify i bind =
       let val namei = if i > 0 then name ^ string_of_int i else name;
       in
diff -r a063a96c8662 -r 541d818d2ff3 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 10:36:00 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Wed Sep 12 11:38:22 2012 +0200
@@ -64,7 +64,7 @@
     val ks = 1 upto n;
     val m = live - n (*passive, if 0 don't generate a new bnf*);
     val ls = 1 upto m;
-    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
+    val b = Binding.name (mk_bundle_name bs);
 
     (* TODO: check if m, n etc are sane *)
 
@@ -1675,7 +1675,7 @@
         map (fn i => map (fn i' =>
           split_conj_thm (if n = 1 then set_rv_Lev' RS mk_conjunctN n i RS mp
             else set_rv_Lev' RS mk_conjunctN n i RS mp RSN
-              (2, @{thm sum_case_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
+              (2, @{thm sum_case_weak_cong} RS @{thm subst[of _ _ "%x. x"]}) RS
               (mk_sum_casesN n i' RS @{thm subst[of _ _ "%x. x"]}))) ks) ks
       end;
 
diff -r a063a96c8662 -r 541d818d2ff3 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 10:36:00 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Wed Sep 12 11:38:22 2012 +0200
@@ -33,7 +33,7 @@
     val n = length bnfs; (*active*)
     val ks = 1 upto n;
     val m = live - n; (*passive, if 0 don't generate a new bnf*)
-    val b = Binding.name (fold_rev (fn b => fn s => Binding.name_of b ^ s) bs "");
+    val b = Binding.name (mk_bundle_name bs);
 
     (* TODO: check if m, n etc are sane *)