diff -r 4a087b9a29c5 -r 679253fef277 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:26:50 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Wed Jan 31 11:40:26 2018 +0100
@@ -30,6 +30,8 @@
   val pos_of_token: token -> Position.T
   val end_pos_of_token: token -> Position.T
   val tokens_match_ord: token * token -> order
+  val literal: string -> token
+  val is_literal: token -> bool
   val is_proper: token -> bool
   val dummy: token
   val mk_eof: Position.T -> token
@@ -154,6 +156,9 @@
     (Literal, Literal) => fast_string_ord (apply2 str_of_token toks)
   | kinds => token_kind_ord kinds);
 
+fun literal s = Token (Literal, s, Position.no_range);
+fun is_literal tok = kind_of_token tok = Literal;
+
 val is_proper = kind_of_token #> (fn Space => false | Comment _ => false | _ => true);
 
 val dummy = Token (Dummy, "", Position.no_range);