src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Mon Apr 18 15:51:48 2016 +0100
+++ b/src/Pure/Isar/token.ML	Mon Apr 18 20:24:19 2016 +0200
@@ -93,6 +93,7 @@
   val explode: Keyword.keywords -> Position.T -> string -> T list
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T
+  val make_int: int -> T list
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
   type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list)
@@ -675,6 +676,8 @@
     val pos' = Position.no_range_position pos;
   in Token ((x, (pos', pos')), y, z) end;
 
+val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
+
 fun make_src a args = make_string a :: args;