1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 12:01:48 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Wed Nov 06 12:47:50 2013 +0100
     1.3 @@ -268,37 +268,23 @@
     1.4      fun massage_call bound_Ts U T =
     1.5        massage_let_if_case ctxt has_call (fn bound_Ts => fn t =>
     1.6          if has_call t then
     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
    1.12 -                val typof = curry fastype_of1 bound_Ts;
    1.13 -                val f' = mk_ctr Us f
    1.14 -                val f'_T = typof f';
    1.15 -                val arg_Ts = map typof args;
    1.16 -              in
    1.17 -                Term.list_comb (f', map3 (massage_call bound_Ts) (binder_types f'_T) arg_Ts args)
    1.18 -              end
    1.19 -            | NONE =>
    1.20 -              (case t of
    1.21 -                Const (@{const_name prod_case}, _) $ t' =>
    1.22 -                let
    1.23 -                  val U' = curried_type U;
    1.24 -                  val T' = curried_type T;
    1.25 -                in
    1.26 -                  Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
    1.27 -                end
    1.28 -              | t1 $ t2 =>
    1.29 -                (if has_call t2 then
    1.30 -                  massage_mutual_call bound_Ts U T t
    1.31 -                else
    1.32 -                  massage_map bound_Ts U T t1 $ t2
    1.33 -                  handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
    1.34 -              | Abs (s, T', t') =>
    1.35 -                Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
    1.36 -              | _ => massage_mutual_call bound_Ts U T t))
    1.37 -          | _ => ill_formed_corec_call ctxt t)
    1.38 +          (case t of
    1.39 +            Const (@{const_name prod_case}, _) $ t' =>
    1.40 +            let
    1.41 +              val U' = curried_type U;
    1.42 +              val T' = curried_type T;
    1.43 +            in
    1.44 +              Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
    1.45 +            end
    1.46 +          | t1 $ t2 =>
    1.47 +            (if has_call t2 then
    1.48 +              massage_mutual_call bound_Ts U T t
    1.49 +            else
    1.50 +              massage_map bound_Ts U T t1 $ t2
    1.51 +              handle AINT_NO_MAP _ => massage_mutual_call bound_Ts U T t)
    1.52 +          | Abs (s, T', t') =>
    1.53 +            Abs (s, T', massage_call (T' :: bound_Ts) (range_type U) (range_type T) t')
    1.54 +          | _ => massage_mutual_call bound_Ts U T t)
    1.55          else
    1.56            build_map_Inl (T, U) $ t) bound_Ts;
    1.57