diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -226,7 +226,7 @@
         "Known modes are " ^ commas_quote (known_modes lthy) ^ "."]);
     val Setup_Data {fixp, mono, fixp_eq, fixp_induct, fixp_induct_user} = setup_data;
 
-    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [eqn_raw] lthy;
+    val ((fixes, [(eq_abinding, eqn)]), _) = prep fixes_raw [(eqn_raw, [])] lthy;
     val ((_, plain_eqn), args_ctxt) = Variable.focus NONE eqn lthy;
 
     val ((f_binding, fT), mixfix) = the_single fixes;
@@ -306,14 +306,14 @@
     |> note_qualified ("fixp_induct", [specialized_fixp_induct])
   end;
 
-val add_partial_function = gen_add_partial_function Specification.check_spec;
-val add_partial_function_cmd = gen_add_partial_function Specification.read_spec;
+val add_partial_function = gen_add_partial_function Specification.check_multi_specs;
+val add_partial_function_cmd = gen_add_partial_function Specification.read_multi_specs;
 
 val mode = @{keyword "("} |-- Parse.name --| @{keyword ")"};
 
 val _ =
   Outer_Syntax.local_theory @{command_keyword partial_function} "define partial function"
-    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+    ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.simple_spec)))
       >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
 
 end;