--- 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