diff -r c9605a284fba -r 2f18172214c8 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Thu Apr 28 09:43:11 2016 +0200
@@ -100,7 +100,7 @@
   val default_config : function_config
   val function_parser : function_config ->
     ((function_config * (binding * string option * mixfix) list) *
-      (Attrib.binding * string) list) parser
+      Specification.multi_specs_cmd) parser
 end
 
 structure Function_Common : FUNCTION_COMMON =
@@ -374,7 +374,7 @@
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
-      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
+      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
 end