--- a/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 14:06:21 2010 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Oct 26 14:11:34 2010 +0200
@@ -228,7 +228,7 @@
val mode = Parse.$$$ "(" |-- Parse.xname --| Parse.$$$ ")";
val _ = Outer_Syntax.local_theory
- "partial_function" "define partial function" Keyword.thy_goal
+ "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));