--- a/src/Pure/Isar/local_theory.ML Sun Dec 24 11:46:20 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML Sun Dec 24 11:51:59 2023 +0100
@@ -30,6 +30,7 @@
local_theory -> local_theory
val restore_background_naming: local_theory -> local_theory -> local_theory
val full_name: local_theory -> binding -> string
+ val bind_name: local_theory -> binding -> string * Position.T
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
val standard_morphism: local_theory -> Proof.context -> morphism
@@ -186,6 +187,7 @@
val restore_background_naming = map_background_naming o K o background_naming_of;
val full_name = Name_Space.full_name o background_naming_of;
+fun bind_name lthy b = (full_name lthy b, Binding.default_pos_of b);
val new_group = map_background_naming Name_Space.new_group;
val reset_group = map_background_naming Name_Space.reset_group;