src/HOL/Tools/Function/partial_function.ML

 val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
 
 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));
 
 
 val setup = Mono_Rules.setup;