# HG changeset patch
# User blanchet
# Date 1473068142 -7200
# Node ID b87d9d2ca67b74c8c5e200500372731b5f998ac7
# Parent  c882ba7412446e0c3f53a002e4011a78ba1c16ee
export more ML functions

diff -r c882ba741244 -r b87d9d2ca67b src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 10:48:06 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Sep 05 11:35:42 2016 +0200
@@ -170,6 +170,17 @@
          * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list)
         * (binding * binding * binding)) * string list) list ->
     Proof.context -> local_theory
+
+  val parse_ctr_arg: (binding * string) parser
+  val parse_ctr_specs: ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list parser
+  val parse_spec: ((((((binding option * (string * string option)) list * binding) * mixfix)
+      * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list)
+    * (binding * binding * binding)) * string list) parser
+  val parse_co_datatype: (Ctr_Sugar.ctr_options_cmd
+        * ((((((binding option * (string * string option)) list * binding) * mixfix)
+      * ((binding, binding * string) Ctr_Sugar.ctr_spec * mixfix) list)
+    * (binding * binding * binding)) * string list) list) parser
+
   val parse_co_datatype_cmd: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
       binding list -> binding list list -> binding list -> (string * sort) list ->
       typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
@@ -2741,8 +2752,8 @@
 fun co_datatypes x = define_co_datatypes (K I) (K I) (K I) (K I) x;
 
 fun co_datatype_cmd x =
-  define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint
-    Syntax.parse_typ Syntax.parse_term x;
+  define_co_datatypes Plugin_Name.make_filter Typedecl.read_constraint Syntax.parse_typ
+    Syntax.parse_term x;
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"}
@@ -2757,6 +2768,7 @@
 
 val parse_co_datatype = parse_ctr_options -- Parse.and_list1 parse_spec;
 
-fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp;
+fun parse_co_datatype_cmd fp construct_fp =
+  parse_co_datatype >> co_datatype_cmd fp construct_fp;
 
 end;