# HG changeset patch # User blanchet # Date 1473322599 -7200 # Node ID adc6ddabfe459982d31720779dfc3e5e17fcc8f9 # Parent 24c4fa81f81c71e15eb9ccfcb1cf91faa4f51fae export ML functions diff -r 24c4fa81f81c -r adc6ddabfe45 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 08 10:16:37 2016 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 08 10:16:39 2016 +0200 @@ -105,6 +105,12 @@ val liveness_of_fp_bnf: int -> BNF_Def.bnf -> bool list val nesting_bnfs: Proof.context -> typ list list list -> typ list -> BNF_Def.bnf list + val massage_simple_notes: string -> (bstring * 'a list * (int -> 'b)) list -> + ((binding * 'c list) * ('a list * 'b) list) list + val massage_multi_notes: string list -> typ list -> + (string * 'a list list * (string -> 'b)) list -> + ((binding * 'b) * ('a list * 'c list) list) list + val define_ctrs_dtrs_for_type: string -> typ -> term -> term -> thm -> thm -> int -> int list -> term -> binding list -> mixfix list -> typ list list -> local_theory -> (term list list * term list * thm * thm list) * local_theory