# HG changeset patch
# User blanchet
# Date 1370415463 -7200
# Node ID 019ca39edd54bf3c45f56e6c6d522a66bc7ae4fc
# Parent  5ef34e96e14a89418a79c2d84e33b3d891c685b3
export ML function (needed for "primrec_new")

diff -r 5ef34e96e14a -r 019ca39edd54 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Jun 04 12:11:48 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Wed Jun 05 08:57:43 2013 +0200
@@ -41,6 +41,7 @@
         * ((term list list * term list list list list * term list list list list)
            * (typ list * typ list list list * typ list list))) option)
     * Proof.context
+  val mk_map: int -> typ list -> typ list -> term -> term
   val build_map: local_theory -> (typ * typ -> term) -> typ * typ -> term
 
   val mk_iter_fun_arg_typessss: typ list -> int list -> int list list -> term ->