--- a/src/HOL/Tools/inductive_set.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Aug 19 23:17:51 2014 +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 * Attrib.src list) list ->
+ (Attrib.binding * string) list -> (Facts.ref * Token.src list) list ->
local_theory -> Inductive.inductive_result * local_theory
val mono_add: attribute
val mono_del: attribute