--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Oct 21 23:35:57 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Oct 21 23:45:27 2013 +0200
@@ -69,6 +69,8 @@
typ list -> term -> term
val massage_nested_corec_call: Proof.context -> (term -> bool) ->
(typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
+ val fold_rev_corec_call: Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> term ->
+ 'a -> string list * 'a
val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
typ list -> term -> term
@@ -471,6 +473,8 @@
if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
end;
+val fold_rev_corec_call = fold_rev_let_if_case;
+
fun expand_to_ctr_term ctxt s Ts t =
(case ctr_sugar_of ctxt s of
SOME {ctrs, casex, ...} =>