# HG changeset patch
# User blanchet
# Date 1379582850 -7200
# Node ID e2c0d0426d2b6c61f419fa56fb349bbc1843d02e
# Parent  aed1ee95cdfe316df6170a88c6199aa8885b7a44
give lambda abstractions a chance, as an alternative to function composition, for corecursion via "fun"

diff -r aed1ee95cdfe -r e2c0d0426d2b src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 03:29:33 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 11:27:30 2013 +0200
@@ -259,23 +259,27 @@
 
     fun massage_call U T =
       massage_let_and_if ctxt has_call (fn t =>
-        (case U of
-          Type (s, Us) =>
-          (case try (dest_ctr ctxt s) t of
-            SOME (f, args) =>
-            let val f' = mk_ctr Us f in
-              list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
-            end
-          | NONE =>
-            (case t of
-              t1 $ t2 =>
-              (if has_call t2 then
-                check_and_massage_direct_call U T t
-              else
-                massage_map U T t1 $ t2
-                handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
-            | _ => check_and_massage_direct_call U T t))
-        | _ => ill_formed_corec_call ctxt t)) U
+        if has_call t then
+          (case U of
+            Type (s, Us) =>
+            (case try (dest_ctr ctxt s) t of
+              SOME (f, args) =>
+              let val f' = mk_ctr Us f in
+                list_comb (f', map3 massage_call (binder_types (typof f')) (map typof args) args)
+              end
+            | NONE =>
+              (case t of
+                t1 $ t2 =>
+                (if has_call t2 then
+                  check_and_massage_direct_call U T t
+                else
+                  massage_map U T t1 $ t2
+                  handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
+              | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t')
+              | _ => check_and_massage_direct_call U T t))
+          | _ => ill_formed_corec_call ctxt t)
+        else
+          build_map_Inl (T, U) $ t) U
   in
     massage_call U (typof t) t
   end;