optimized "mk_case_disc_tac"

--- a/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -242,13 +242,14 @@
                   (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
             ms disc_defs;
 
-        val disc_thmss =
+        val (disc_thmss', disc_thmss) =
           let
             fun mk_thm discI _ [] = refl RS discI
               | mk_thm _ not_disc [distinct] = distinct RS not_disc;
             fun mk_thms discI not_disc distinctss = map (mk_thm discI not_disc) distinctss;
           in
             map3 mk_thms discI_thms not_disc_thms (transpose distinct_thmsss)
+            |> `transpose
           end;
 
         val disc_disjoint_thms =
@@ -266,7 +267,7 @@
               map3 (fn [] => K (K [])
                      | [(((m, discD), _), _)] => fn disc_thm => fn [goal] =>
                 [prove (mk_half_disc_disjoint_tac m discD disc_thm) goal])
-              half_pairss (flat (transpose disc_thmss)) goal_halvess;
+              half_pairss (flat disc_thmss') goal_halvess;
 
             val goal_other_halvess = map (map (mk_goal o swap)) half_pairss;
             val other_half_thmss =
@@ -307,7 +308,7 @@
             val goal = mk_Trueprop_eq (caseofB_fs $ v, mk_rhs discs fs selss);
           in
             Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-              mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss sel_thmss)
+              mk_case_disc_tac ctxt exhaust_thm' case_thms disc_thmss' sel_thmss)
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
 

--- a/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_sugar_tactics.ML	Fri Aug 31 15:04:03 2012 +0200
@@ -21,6 +21,7 @@
 structure BNF_Sugar_Tactics : BNF_SUGAR_TACTICS =
 struct
 
+open BNF_Util
 open BNF_Tactics
 open BNF_FP_Util
 
@@ -58,14 +59,13 @@
       SELECT_GOAL (Local_Defs.unfold_tac ctxt sel_thms) THEN'
       rtac refl)) 1;
 
-fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss sel_thmss =
-  let val base_unfolds = @{thms if_True if_False} @ maps (map eq_True_or_False) disc_thmss in (*###*)
-    (rtac exhaust' THEN'
-     EVERY' (map2 (fn case_thm => fn sel_thms => EVERY' [
-       hyp_subst_tac THEN'
-       SELECT_GOAL (Local_Defs.unfold_tac ctxt (base_unfolds @ sel_thms)) THEN'
-       rtac case_thm]) case_thms sel_thmss)) 1
-  end;
+fun mk_case_disc_tac ctxt exhaust' case_thms disc_thmss' sel_thmss =
+  (rtac exhaust' THEN'
+   EVERY' (map3 (fn case_thm => fn disc_thms => fn sel_thms => EVERY' [
+     hyp_subst_tac THEN'
+     SELECT_GOAL (Local_Defs.unfold_tac ctxt
+       (@{thms if_True if_False} @ disc_thms @ sel_thms)) THEN'
+     rtac case_thm]) case_thms (map (map eq_True_or_False) disc_thmss') sel_thmss)) 1;
 
 fun mk_case_cong_tac exhaust' case_thms =
   (rtac exhaust' THEN'