--- a/src/Pure/Isar/specification.ML Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/specification.ML Tue Aug 19 23:17:51 2014 +0200
@@ -51,11 +51,11 @@
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 * Attrib.src list) list) list ->
+ (Attrib.binding * (thm list * Token.src list) list) list ->
(binding * typ option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorems_cmd: string ->
- (Attrib.binding * (Facts.ref * Attrib.src list) list) list ->
+ (Attrib.binding * (Facts.ref * Token.src list) list) list ->
(binding * string option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorem: string -> Method.text option ->