--- 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}