src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Sat May 20 21:48:41 2023 +0200
+++ b/src/Pure/Isar/token.ML	Sat May 20 22:41:37 2023 +0200
@@ -104,6 +104,7 @@
   val print_properties: Keyword.keywords -> Properties.T -> string
   val make: (int * int) * string -> Position.T -> T * Position.T
   val make_string: string * Position.T -> T
+  val make_string0: string -> T
   val make_int: int -> T list
   val make_src: string * Position.T -> T list -> src
   type 'a parser = T list -> 'a * T list
@@ -771,6 +772,8 @@
     val pos' = Position.no_range_position pos;
   in Token ((x, (pos', pos')), y, z) end;
 
+fun make_string0 s = make_string (s, Position.none);
+
 val make_int = explode Keyword.empty_keywords Position.none o signed_string_of_int;
 
 fun make_src a args = make_string a :: args;