src/Pure/Isar/attrib.ML

   let val (a, context') = Token.syntax_generic scan src context in a (context', th) end;
 
 fun setup binding scan comment = define_global binding (attribute_syntax scan) comment #> snd;
 fun local_setup binding scan comment = define binding (attribute_syntax scan) comment #> snd;
 
-fun attribute_setup name source comment =
+fun attribute_setup (name, pos) source comment =
   ML_Lex.read_source source
-  |> 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) ^
+  |> ML_Context.expression ("parser", pos) "Thm.attribute context_parser"
+    ("Context.map_proof (Attrib.local_setup " ^
+      ML_Syntax.atomic (ML_Syntax.make_binding (name, pos)) ^
       " parser " ^ ML_Syntax.print_string comment ^ ")")
   |> Context.proof_map;
 
 
 (* internal attribute *)