src/Pure/Isar/attrib.ML
changeset 62795 063d2f23cdf6
parent 62498 5dfcc9697f29
child 62878 1cec457e0a03
--- a/src/Pure/Isar/attrib.ML	Fri Apr 01 17:13:40 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 01 17:14:27 2016 +0200
@@ -153,9 +153,7 @@
   let
     val _ =
       if Token.checked_src src then ()
-      else
-        Context_Position.report ctxt
-          (Position.set_range (Token.range_of src)) Markup.language_attribute;
+      else Context_Position.report ctxt (#1 (Token.range_of src)) Markup.language_attribute;
   in #1 (Token.check_src ctxt get_attributes src) end;
 
 val attribs =