src/HOL/Tools/Function/function_common.ML

   val import_function_data : term -> Proof.context -> info option
   val import_last_function : Proof.context -> info option
   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 =
 struct
 

   fun config_parser default =
     (Scan.optional (@{keyword "("} |-- Parse.!!! (Parse.list1 option_parser) --| @{keyword ")"}) [])
      >> (fn opts => fold apply_opt opts default)
 in
   fun function_parser default_cfg =
-      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_alt_specs
-end
-
-
-end
-end
+      config_parser default_cfg -- Parse.fixes -- Parse_Spec.where_multi_specs
+end
+
+
+end
+end