src/HOL/Tools/function_package/fundef_package.ML
changeset 27353 71c4dd53d4cb
parent 27187 17b63e145986
child 28083 103d9282a946
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 14:54:45 2008 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Jun 25 17:38:32 2008 +0200
     1.3 @@ -193,7 +193,7 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 -val _ = OuterSyntax.keywords ["otherwise"];
     1.8 +val _ = OuterKeyword.keyword "otherwise";
     1.9  
    1.10  val _ =
    1.11    OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal