changeset 55916 | 0ac57f18a4b9 |
parent 55915 | 607948c90bf0 |
child 55919 | 2eb8c13339a5 |
--- a/src/Pure/Isar/token.ML Wed Mar 05 14:19:54 2014 +0100 +++ b/src/Pure/Isar/token.ML Wed Mar 05 15:24:06 2014 +0100 @@ -336,10 +336,8 @@ (case get_value tok of NONE => [] | SOME v => - if is_kind Keyword tok then [] - else - let val pos = pos_of tok - in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end); + let val pos = pos_of tok + in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end); (* make values *)