--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 19:58:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Tue Oct 01 22:50:42 2013 +0200
@@ -303,6 +303,8 @@
val massage_direct_corec_call = massage_let_if_case;
+fun curried_type (Type (@{type_name fun}, [Type (@{type_name prod}, Ts), T])) = Ts ---> T;
+
fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
let
val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
@@ -356,7 +358,14 @@
end
| NONE =>
(case t of
- t1 $ t2 =>
+ Const (@{const_name prod_case}, _) $ t' =>
+ let
+ val U' = curried_type U;
+ val T' = curried_type T;
+ in
+ Const (@{const_name prod_case}, U' --> U) $ massage_call bound_Ts U' T' t'
+ end
+ | t1 $ t2 =>
(if has_call t2 then
massage_direct_call bound_Ts U T t
else