Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/function_package/fundef_common.ML
changeset 25045 12386aefe9ac
parent 24920 2a45e400fdad
child 25201 e6fe58b640ce 
--- 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)
isabelle