# HG changeset patch
# User blanchet
# Date 1382391927 -7200
# Node ID 5288fa24c9db064f28a70e16288250757cd96b8e
# Parent  80259d79a81e78bb9ac2031e0031a8357246c3a2
made lower-level function available

diff -r 80259d79a81e -r 5288fa24c9db src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- 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, ...} =>