# HG changeset patch
# User krauss
# Date 1192536666 -7200
# Node ID 12386aefe9aca40ae790bd945e7286dcdfa62c44
# Parent  de1f50ab668d824d7c2650e735064585c551f190
"sequential" is no longer a keyword. It is still used as before, but as a normal
identifier => no pollution of keyword space

diff -r de1f50ab668d -r 12386aefe9ac src/HOL/Tools/function_package/fundef_common.ML
--- 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)
diff -r de1f50ab668d -r 12386aefe9ac src/HOL/Tools/function_package/fundef_package.ML
--- 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