# HG changeset patch
# User traytel
# Date 1378635965 -7200
# Node ID 3356a148b78372fe8f3c0e77deb667e1e5ba3d92
# Parent  0688928a41fdce1c20acf3af868e3efd4105d053
don't register "sequential" as a keyword for now as this breaks the parser for function

diff -r 0688928a41fd -r 3356a148b783 etc/isar-keywords.el
--- 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"
diff -r 0688928a41fd -r 3356a148b783 src/HOL/BNF/BNF_GFP.thy
--- 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"
diff -r 0688928a41fd -r 3356a148b783 src/HOL/BNF/Tools/bnf_gfp.ML
--- 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;