"sequential" is no longer a keyword. It is still used as before, but as a normal
identifier => no pollution of keyword space

--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 16 13:00:13 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Oct 16 14:11:06 2007 +0200
@@ -294,9 +294,7 @@
 local 
   structure P = OuterParse and K = OuterKeyword 
 
-  val opt_sequential = Scan.optional ((P.$$$ "(" |-- P.$$$ "sequential" --| P.$$$ ")") >> K true) false
-                       
-  val option_parser = (P.$$$ "sequential" >> K Sequential)
+  val option_parser = (P.reserved "sequential" >> K Sequential)
                    || ((P.reserved "default" |-- P.term) >> Default)
                    || (P.reserved "domintros" >> K DomIntros)
                    || (P.reserved "tailrec" >> K Tailrec)

--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 16 13:00:13 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 16 14:11:06 2007 +0200
@@ -268,7 +268,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-val _ = OuterSyntax.keywords ["sequential", "otherwise"];
+val _ = OuterSyntax.keywords ["otherwise"];
 
 val _ =
   OuterSyntax.command "function" "define general recursive functions" K.thy_goal