src/HOL/Tools/function_package/fundef_package.ML
changeset 25045 12386aefe9ac
parent 24977 9f98751c9628
child 25088 9a13ab12b174
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 16 13:00:13 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Oct 16 14:11:06 2007 +0200
     1.3 @@ -268,7 +268,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val _ = OuterSyntax.keywords ["sequential", "otherwise"];
     1.8 +val _ = OuterSyntax.keywords ["otherwise"];
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.command "function" "define general recursive functions" K.thy_goal