put an underscore between names, for compatibility with old package (and also because it makes sense)

--- 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

--- 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;
 

--- 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 *)