1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:52:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Wed Sep 25 16:57:48 2013 +0200
     1.3 @@ -371,10 +371,7 @@
     1.4    (case fastype_of1 (bound_Ts, t) of
     1.5      Type (s, Ts) =>
     1.6      massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
     1.7 -      if can (dest_ctr ctxt s) t then
     1.8 -        t
     1.9 -      else
    1.10 -        massage_let_if_case ctxt has_call (K I) bound_Ts (expand_ctr_term ctxt s Ts t)) bound_Ts t
    1.11 +      if can (dest_ctr ctxt s) t then t else expand_ctr_term ctxt s Ts t) bound_Ts t
    1.12    | _ => raise Fail "expand_corec_code_rhs");
    1.13  
    1.14  fun massage_corec_code_rhs ctxt massage_ctr =