# HG changeset patch
# User blanchet
# Date 1370340708 -7200
# Node ID 5ef34e96e14a89418a79c2d84e33b3d891c685b3
# Parent  b7c8675437ecc489cd5143c9620d0fbe0cc49725
export ML function

diff -r b7c8675437ec -r 5ef34e96e14a src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Jun 03 11:37:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Jun 04 12:11:48 2013 +0200
@@ -27,6 +27,7 @@
 
   val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list
   val exists_subtype_in: typ list -> typ -> bool
+  val flat_rec: ('a -> 'b list) -> 'a list -> 'b list
   val mk_co_iter: theory -> BNF_FP_Util.fp_kind -> typ -> typ list -> term -> term
   val nesty_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list
   val indexify_fst: ''a list -> (int -> ''a * 'b -> 'c) -> ''a * 'b -> 'c