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 =