don't register "sequential" as a keyword for now as this breaks the parser for function
--- a/etc/isar-keywords.el Sat Sep 07 23:09:26 2013 +0200
+++ b/etc/isar-keywords.el Sun Sep 08 12:26:05 2013 +0200
@@ -350,7 +350,6 @@
"permissive"
"pervasive"
"rep_compat"
- "sequential"
"shows"
"structure"
"type_class"
--- a/src/HOL/BNF/BNF_GFP.thy Sat Sep 07 23:09:26 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Sun Sep 08 12:26:05 2013 +0200
@@ -11,8 +11,7 @@
imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
keywords
"codatatype" :: thy_decl and
- "primcorec" :: thy_goal and
- "sequential"
+ "primcorec" :: thy_goal
begin
lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Sat Sep 07 23:09:26 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Sun Sep 08 12:26:05 2013 +0200
@@ -2903,9 +2903,17 @@
Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
+local
+
+val option_parser = Parse.group (fn () => "option") (Parse.reserved "sequential" >> K true);
+
+in
+
val _ = Outer_Syntax.local_theory_to_proof @{command_spec "primcorec"}
"define primitive corecursive functions"
- ((Scan.option @{keyword "sequential"} >> is_some) --
+ ((Scan.optional (@{keyword "("} |-- Parse.!!! option_parser --| @{keyword ")"}) false) --
(Parse.fixes -- Parse_Spec.where_alt_specs) >> uncurry add_primcorec_cmd);
+
+end
end;