src/Pure/Isar/token.ML
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 *)