diff -r c20946f5b6fb -r e9c777bfd78c src/HOL/Tools/Function/partial_function.ML --- a/src/HOL/Tools/Function/partial_function.ML Sat Jun 11 13:57:59 2016 +0200 +++ b/src/HOL/Tools/Function/partial_function.ML Sat Jun 11 16:41:11 2016 +0200 @@ -313,7 +313,7 @@ val _ = Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function" - ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec))) - >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec)); + ((mode -- (Parse.vars -- (Parse.where_ |-- Parse_Spec.simple_spec))) + >> (fn (mode, (vars, spec)) => add_partial_function_cmd mode vars spec)); end;