diff -r 343905de27b1 -r b8ffc3dc9e24 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -309,7 +309,7 @@
 val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
 
 val _ =
-  Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+  Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
     ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
       >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));