# HG changeset patch
# User blanchet
# Date 1393192271 -3600
# Node ID 1f9cc432ecd4975505fbb7dcfca109b95629bc41
# Parent  e42e5671612c2e116ae6a67e10e5379704eb417e
reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'

diff -r e42e5671612c -r 1f9cc432ecd4 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 21:53:01 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -86,7 +86,7 @@
     local_theory -> gfp_sugar_thms
 
   type co_datatype_spec =
-    ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+    ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
     * ((binding, binding * typ, term) Ctr_Sugar.ctr_spec * mixfix) list
 
   val co_datatypes: BNF_Util.fp_kind -> (mixfix list -> binding list -> binding list ->
@@ -285,7 +285,7 @@
   handle THM _ => thm;
 
 type co_datatype_spec =
-  ((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
+  ((((binding option * (typ * sort)) list * binding) * (binding * binding)) * mixfix)
   * ((binding, binding * typ, term) ctr_spec * mixfix) list;
 
 fun type_args_named_constrained_of_spec ((((ncAs, _), _), _), _) = ncAs;
@@ -972,7 +972,9 @@
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
     val num_As = length unsorted_As;
-    val set_bss = map (map fst o type_args_named_constrained_of_spec) specs;
+
+    val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
+    val set_bss = map (map (the_default Binding.empty)) set_boss;
 
     val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
@@ -1471,18 +1473,6 @@
 fun co_datatype_cmd x =
   define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term x;
 
-val parse_type_arg_constrained =
-  Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
-
-val parse_type_arg_named_constrained = parse_opt_binding_colon -- parse_type_arg_constrained;
-
-(*FIXME: use parse_type_args_named_constrained from BNF_Util and thus 
-  allow users to kill certain arguments of a (co)datatype*)
-val parse_type_args_named_constrained =
-  parse_type_arg_constrained >> (single o pair Binding.empty) ||
-  @{keyword "("} |-- Parse.!!! (Parse.list1 parse_type_arg_named_constrained --| @{keyword ")"}) ||
-  Scan.succeed [];
-
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
   (Parse.typ >> pair Binding.empty);