1.1 --- a/src/ZF/Tools/datatype_package.ML	Thu Mar 15 19:48:19 2012 +0100
     1.2 +++ b/src/ZF/Tools/datatype_package.ML	Thu Mar 15 20:07:00 2012 +0100
     1.3 @@ -427,15 +427,15 @@
     1.4    #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
     1.5  
     1.6  val con_decl =
     1.7 -  Parse.name -- Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.term --| Parse.$$$ ")") [] --
     1.8 +  Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
     1.9      Parse.opt_mixfix >> Parse.triple1;
    1.10  
    1.11  val datatype_decl =
    1.12 -  (Scan.optional ((Parse.$$$ "\<subseteq>" || Parse.$$$ "<=") |-- Parse.!!! Parse.term) "") --
    1.13 -  Parse.and_list1 (Parse.term -- (Parse.$$$ "=" |-- Parse.enum1 "|" con_decl)) --
    1.14 -  Scan.optional (Parse.$$$ "monos" |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.15 -  Scan.optional (Parse.$$$ "type_intros" |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.16 -  Scan.optional (Parse.$$$ "type_elims" |-- Parse.!!! Parse_Spec.xthms1) []
    1.17 +  (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
    1.18 +  Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
    1.19 +  Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.20 +  Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
    1.21 +  Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
    1.22    >> (Toplevel.theory o mk_datatype);
    1.23  
    1.24  val coind_prefix = if coind then "co" else "";