# 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;