# 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