diff -r 8a881f83e206 -r 42ac3cfb89f6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Mar 01 19:55:01 2014 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Mar 01 22:46:31 2014 +0100
@@ -35,8 +35,7 @@
     Context.generic -> (string * thm list) list * Context.generic
   val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
-  val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
-    theory -> theory
+  val attribute_setup: bstring * Position.T -> Symbol_Pos.source -> string -> theory -> theory
   val internal: (morphism -> attribute) -> src
   val add_del: attribute -> attribute -> attribute context_parser
   val thm_sel: Facts.interval list parser
@@ -185,12 +184,12 @@
   add_attribute name
     (fn src => fn (ctxt, th) => let val (a, ctxt') = syntax scan src ctxt in a (ctxt', th) end);
 
-fun attribute_setup name (txt, pos) cmt =
-  Context.theory_map (ML_Context.expression pos
+fun attribute_setup name source cmt =
+  Context.theory_map (ML_Context.expression (#pos source)
     "val (name, scan, comment): binding * attribute context_parser * string"
     "Context.map_theory (Attrib.setup name scan comment)"
     (ML_Lex.read Position.none ("(" ^ ML_Syntax.make_binding name ^ ", ") @
-      ML_Lex.read pos txt @
+      ML_Lex.read_source source @
       ML_Lex.read Position.none (", " ^ ML_Syntax.print_string cmt ^ ")")));