src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

     term
   val massage_indirect_corec_call: Proof.context -> (term -> bool) ->
     (typ -> typ -> term -> term) -> typ list -> typ -> term -> term
   val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
   val massage_corec_code_rhs: Proof.context -> (term -> term list -> term) -> typ -> term -> term
+  val fold_rev_corec_code_rhs: (term -> term list -> 'a -> 'a) -> term -> 'a -> 'a
   val simplify_bool_ifs: theory -> term -> term list
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
     (bool * rec_spec list * typ list * thm * thm list) * local_theory
   val corec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->

       | (Const (@{const_name If}, _), arg :: args) =>
         list_comb (If_const U $ tap check_cond arg, map massage_rec args)
       | _ => massage_leaf t)
   in
     massage_rec
+  end;
+
+fun fold_rev_let_and_if f =
+  let
+    fun fld t =
+      (case Term.strip_comb t of
+        (Const (@{const_name Let}, _), [arg1, arg2]) => fld (betapply (arg2, arg1))
+      | (Const (@{const_name If}, _), _ :: args) => fold_rev fld args
+      | _ => f t)
+  in
+    fld
   end;
 
 fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
   massage_let_and_if ctxt has_call massage_direct_call U t;
 

   | _ => raise Fail "expand_corec_code_rhs");
 
 fun massage_corec_code_rhs ctxt massage_ctr =
   massage_let_and_if ctxt (K false) (uncurry massage_ctr o Term.strip_comb);
 
+fun fold_rev_corec_code_rhs f = fold_rev_let_and_if (uncurry f o Term.strip_comb);
+
 fun add_conjuncts (Const (@{const_name conj}, _) $ t $ t') = add_conjuncts t o add_conjuncts t'
   | add_conjuncts t = cons t;
 
 fun conjuncts t = add_conjuncts t [];