--- a/src/Pure/Isar/specification.ML Thu Jun 09 11:40:39 2016 +0200
+++ b/src/Pure/Isar/specification.ML Thu Jun 09 12:02:38 2016 +0200
@@ -51,7 +51,7 @@
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * Attrib.thms) list ->
(binding * typ option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorems_cmd: string ->