--- a/src/HOL/Tools/Function/fun.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/Function/fun.ML Thu Apr 28 09:43:11 2016 +0200
@@ -9,10 +9,10 @@
sig
val fun_config : Function_Common.function_config
val add_fun : (binding * typ option * mixfix) list ->
- (Attrib.binding * term) list -> Function_Common.function_config ->
+ Specification.multi_specs -> Function_Common.function_config ->
local_theory -> Proof.context
val add_fun_cmd : (binding * string option * mixfix) list ->
- (Attrib.binding * string) list -> Function_Common.function_config ->
+ Specification.multi_specs_cmd -> Function_Common.function_config ->
bool -> local_theory -> Proof.context
end