diff -r f19e5837ad69 -r 5c6955f487e5 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -281,10 +281,10 @@
 
 val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
 
-val _ = Outer_Syntax.local_theory
-  "partial_function" "define partial function" Keyword.thy_decl
-  ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
-     >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
+val _ =
+  Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+      >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
 
 val setup = Mono_Rules.setup;