--- a/src/HOL/Tools/inductive_set.ML Wed Apr 27 10:03:35 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Apr 28 09:43:11 2016 +0200
@@ -20,7 +20,7 @@
val add_inductive: bool -> bool ->
(binding * string option * mixfix) list ->
(binding * string option * mixfix) list ->
- (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
+ Specification.multi_specs_cmd -> (Facts.ref * Token.src list) list ->
local_theory -> Inductive.inductive_result * local_theory
val mono_add: attribute
val mono_del: attribute