# HG changeset patch
# User blanchet
# Date 1380660642 -7200
# Node ID 769fcbdf2918095296ef84a8ba4dab7692d034d1
# Parent  a29ea2c5160d0c82c49ec957eee105c4693bc508
allow uncurried lambda-abstractions on rhs of "primcorec"

diff -r a29ea2c5160d -r 769fcbdf2918 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- 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