# HG changeset patch
# User wenzelm
# Date 1684615297 -7200
# Node ID 79ad3181071b2f5299ae53d62474afd9be31f7ee
# Parent  52d071212a7a660adb931df26b26424334885c3f
tuned signature;

diff -r 52d071212a7a -r 79ad3181071b src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sat May 20 21:48:41 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sat May 20 22:41:37 2023 +0200
@@ -245,9 +245,7 @@
 
     val dummy_thm = Thm.transfer thy Drule.dummy_thm
     val restore_lifting_att = 
-      ([dummy_thm],
-        [map (Token.make_string o rpair Position.none)
-          ["Lifting.lifting_restore_internal", bundle_name]])
+      ([dummy_thm], [map Token.make_string0 ["Lifting.lifting_restore_internal", bundle_name]])
   in
     lthy
     |> Local_Theory.declaration {syntax = false, pervasive = true}
diff -r 52d071212a7a -r 79ad3181071b 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;