# 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 ->