diff -r 568840962230 -r bc6bced136e5 src/Pure/Isar/specification.ML
--- 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 ->