1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 03:13:13 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 19 03:29:33 2013 +0200
     1.3 @@ -59,6 +59,7 @@
     1.4      (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
     1.5    val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
     1.6    val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ -> term -> term
     1.7 +  val fold_rev_corec_code_rhs: (term -> term list -> 'a -> 'a) -> term -> 'a -> 'a
     1.8    val simplify_bool_ifs: theory -> term -> term list
     1.9    val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
    1.10      ((term * term list list) list) list -> local_theory ->
    1.11 @@ -209,6 +210,17 @@
    1.12      massage_rec
    1.13    end;
    1.14  
    1.15 +fun fold_rev_let_and_if f =
    1.16 +  let
    1.17 +    fun fld t =
    1.18 +      (case Term.strip_comb t of
    1.19 +        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
    1.20 +      | (Const (@{const_name If}, _), _ :: args) => fold_rev fld args
    1.21 +      | _ => f t)
    1.22 +  in
    1.23 +    fld
    1.24 +  end;
    1.25 +
    1.26  fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
    1.27    massage_let_and_if ctxt has_call massage_direct_call U t;
    1.28  
    1.29 @@ -298,6 +310,8 @@
    1.30  fun massage_corec_code_rhs ctxt massage_ctr =
    1.31    massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
    1.32  
    1.33 +fun fold_rev_corec_code_rhs f = fold_rev_let_and_if (uncurry f o Term.strip_comb);
    1.34 +
    1.35  fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
    1.36    | add_conjuncts t = cons t;
    1.37