diff -r b3c45d0e4fe1 -r a8bcb5a446c8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Nov 29 14:43:10 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Nov 30 12:24:56 2014 +0100
@@ -41,7 +41,7 @@
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
   val local_setup: Binding.binding -> attribute context_parser -> string ->
     local_theory -> local_theory
-  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string ->
+  val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
   val internal: (morphism -> attribute) -> Token.src
   val add_del: attribute -> attribute -> attribute context_parser
@@ -49,7 +49,7 @@
   val thms: thm list context_parser
   val multi_thm: thm list context_parser
   val check_attribs: Proof.context -> Token.src list -> Token.src list
-  val read_attribs: Proof.context -> Symbol_Pos.source -> Token.src list
+  val read_attribs: Proof.context -> Input.source -> Token.src list
   val transform_facts: morphism ->
     (Attrib.binding * (thm list * Token.src list) list) list ->
     (Attrib.binding * (thm list * Token.src list) list) list
@@ -208,7 +208,7 @@
 
 fun attribute_setup name source comment =
   ML_Lex.read_source false source
-  |> ML_Context.expression (#range source) "parser" "Thm.attribute context_parser"
+  |> ML_Context.expression (Input.range_of source) "parser" "Thm.attribute context_parser"
     ("Context.map_proof (Attrib.local_setup " ^ ML_Syntax.atomic (ML_Syntax.make_binding name) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
@@ -287,11 +287,11 @@
 fun read_attribs ctxt source =
   let
     val keywords = Thy_Header.get_keywords' ctxt;
-    val syms = Symbol_Pos.source_explode source;
+    val syms = Input.source_explode source;
   in
     (case Token.read_no_commands keywords Parse.attribs syms of
       [raw_srcs] => check_attribs ctxt raw_srcs
-    | _ => error ("Malformed attributes" ^ Position.here (#1 (#range source))))
+    | _ => error ("Malformed attributes" ^ Position.here (Input.pos_of source)))
   end;