src/HOL/Tools/Function/function_common.ML

   val transform_function_data : morphism -> info -> info
   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) *
-      Specification.multi_specs_cmd) parser
+    (function_config * ((binding * string option * mixfix) list * 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_multi_specs
-end
-
-
-end
-end
+      config_parser default_cfg -- Parse_Spec.specification
+end
+
+
+end
+end