1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 03:29:33 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 11:27:30 2013 +0200
     1.3 @@ -259,23 +259,27 @@
     1.4  
     1.5      fun massage_call U T =
     1.6        massage_let_and_if ctxt has_call (fn t =>
     1.7 -        (case U of
     1.8 -          Type (s, Us) =>
     1.9 -          (case try (dest_ctr ctxt s) t of
    1.10 -            SOME (f, args) =>
    1.11 -            let val f' = mk_ctr Us f in
    1.12 -              list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
    1.13 -            end
    1.14 -          | NONE =>
    1.15 -            (case t of
    1.16 -              t1 $ t2 =>
    1.17 -              (if has_call t2 then
    1.18 -                check_and_massage_direct_call U T t
    1.19 -              else
    1.20 -                massage_map U T t1 $ t2
    1.21 -                handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
    1.22 -            | _ => check_and_massage_direct_call U T t))
    1.23 -        | _ => ill_formed_corec_call ctxt t)) U
    1.24 +        if has_call t then
    1.25 +          (case U of
    1.26 +            Type (s, Us) =>
    1.27 +            (case try (dest_ctr ctxt s) t of
    1.28 +              SOME (f, args) =>
    1.29 +              let val f' = mk_ctr Us f in
    1.30 +                list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
    1.31 +              end
    1.32 +            | NONE =>
    1.33 +              (case t of
    1.34 +                t1 $ t2 =>
    1.35 +                (if has_call t2 then
    1.36 +                  check_and_massage_direct_call U T t
    1.37 +                else
    1.38 +                  massage_map U T t1 $ t2
    1.39 +                  handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
    1.40 +              | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t')
    1.41 +              | _ => check_and_massage_direct_call U T t))
    1.42 +          | _ => ill_formed_corec_call ctxt t)
    1.43 +        else
    1.44 +          build_map_Inl (T, U) $ t) U
    1.45    in
    1.46      massage_call U (typof t) t
    1.47    end;