1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 21 23:35:57 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Mon Oct 21 23:45:27 2013 +0200
     1.3 @@ -69,6 +69,8 @@
     1.4      typ list -> term -> term
     1.5    val massage_nested_corec_call: Proof.context -> (term -> bool) ->
     1.6      (typ list -> typ -> typ -> term -> term) -> typ list -> typ -> term -> term
     1.7 +  val fold_rev_corec_call:  Proof.context -> (term list -> term -> 'a -> 'a) -> typ list -> term ->
     1.8 +    'a -> string list * 'a
     1.9    val expand_corec_code_rhs: Proof.context -> (term -> bool) -> typ list -> term -> term
    1.10    val massage_corec_code_rhs: Proof.context -> (typ list -> term -> term list -> term) ->
    1.11      typ list -> term -> term
    1.12 @@ -471,6 +473,8 @@
    1.13      if has_call t then massage_call bound_Ts U T t else build_map_Inl (T, U) $ t
    1.14    end;
    1.15  
    1.16 +val fold_rev_corec_call = fold_rev_let_if_case;
    1.17 +
    1.18  fun expand_to_ctr_term ctxt s Ts t =
    1.19    (case ctr_sugar_of ctxt s of
    1.20      SOME {ctrs, casex, ...} =>