1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 17:52:01 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 18:29:55 2012 +0200
     1.3 @@ -22,10 +22,11 @@
     1.4  
     1.5  open BNF_Tactics
     1.6  open BNF_Util
     1.7 +open BNF_FP_Util
     1.8  
     1.9  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    1.10    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    1.11 -  (rtac (BNF_FP_Util.mk_sum_casesN n k RS ssubst) THEN'
    1.12 +  (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    1.13     REPEAT_DETERM_N (Int.max (0, m - 1)) o rtac (@{thm split} RS ssubst) THEN'
    1.14     rtac refl) 1;
    1.15