1.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Nov 25 18:18:58 2013 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Mon Nov 25 20:25:22 2013 +0100
     1.3 @@ -2921,19 +2921,23 @@
     1.4    Outer_Syntax.local_theory @{command_spec "codatatype"} "define coinductive datatypes"
     1.5      (parse_co_datatype_cmd Greatest_FP construct_gfp);
     1.6  
     1.7 -val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
     1.8 +val option_parser = Parse.group (fn () => "option")
     1.9 +  ((Parse.reserved "sequential" >> K Option_Sequential)
    1.10 +  || (Parse.reserved "exhaustive" >> K Option_Exhaustive))
    1.11  
    1.12  val where_alt_specs_of_parser = Parse.where_ |-- Parse.!!! (Parse.enum1 "|"
    1.13    (Parse_Spec.spec -- Scan.option (Parse.reserved "of" |-- Parse.const)));
    1.14  
    1.15  val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorecursive"}
    1.16    "define primitive corecursive functions"
    1.17 -  ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    1.18 +  ((Scan.optional (@{keyword "("} |--
    1.19 +      Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
    1.20      (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorecursive_cmd);
    1.21  
    1.22  val _ = Outer_Syntax.local_theory @{command_spec "primcorec"}
    1.23    "define primitive corecursive functions"
    1.24 -  ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
    1.25 +  ((Scan.optional (@{keyword "("} |--
    1.26 +      Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) []) --
    1.27      (Parse.fixes -- where_alt_specs_of_parser) >> uncurry add_primcorec_cmd);
    1.28  
    1.29  end;