started work on sugared "(co)data" commands

--- a/etc/isar-keywords.el	Tue Sep 04 13:02:25 2012 +0200
+++ b/etc/isar-keywords.el	Tue Sep 04 13:02:26 2012 +0200
@@ -47,6 +47,7 @@
     "class_deps"
     "classes"
     "classrel"
+    "codata"
     "codata_raw"
     "code_abort"
     "code_class"
@@ -69,6 +70,7 @@
     "context"
     "corollary"
     "cpodef"
+    "data"
     "data_raw"
     "datatype"
     "declaration"
@@ -475,6 +477,7 @@
     "class"
     "classes"
     "classrel"
+    "codata"
     "codata_raw"
     "code_abort"
     "code_class"
@@ -491,6 +494,7 @@
     "coinductive_set"
     "consts"
     "context"
+    "data"
     "data_raw"
     "datatype"
     "declaration"

--- a/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:02:25 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy	Tue Sep 04 13:02:26 2012 +0200
@@ -11,6 +11,12 @@
 
 theory Codatatype
 imports BNF_Wrap BNF_LFP BNF_GFP
+keywords
+  "data" :: thy_decl
+and
+  "codata" :: thy_decl
+uses
+  "Tools/bnf_fp_sugar.ML"
 begin
 
 end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 04 13:02:26 2012 +0200
@@ -0,0 +1,39 @@
+(*  Title:      HOL/Codatatype/Tools/bnf_fp_sugar.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Sugar for constructing LFPs and GFPs.
+*)
+
+signature BNF_FP_SUGAR =
+sig
+end;
+
+structure BNF_FP_Sugar : BNF_FP_SUGAR =
+struct
+
+fun data_cmd gfp specs lthy =
+  let
+  in
+    lthy
+  end;
+
+val parse_ctr_arg =
+  Parse.$$$ "(" |-- Scan.option Parse.binding --| Parse.$$$ ":" -- Parse.typ --| Parse.$$$ ")" ||
+  (Parse.typ >> pair NONE);
+
+val parse_single_spec =
+  Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
+  (@{keyword "="} |-- Parse.enum1 "|" (Parse.binding -- Scan.repeat parse_ctr_arg --
+     Parse.opt_mixfix))
+  >> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
+    (Parse.and_list1 parse_single_spec >> data_cmd false);
+
+val _ =
+  Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
+    (Parse.and_list1 parse_single_spec >> data_cmd true);
+
+end;