1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 27 17:57:45 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Fri Sep 27 19:30:49 2013 +0200
     1.3 @@ -368,8 +368,10 @@
     1.4            | _ => ill_formed_corec_call ctxt t)
     1.5          else
     1.6            build_map_Inl (T, U) $ t) bound_Ts;
     1.7 +
     1.8 +    val T = fastype_of1 (bound_Ts, t);
     1.9    in
    1.10 -    massage_call bound_Ts U (fastype_of1 (bound_Ts, t)) t
    1.11 +    if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
    1.12    end;
    1.13  
    1.14  fun expand_ctr_term ctxt s Ts t =