--- a/src/Pure/Isar/local_theory.ML Wed Dec 27 13:02:22 2023 +0100
+++ b/src/Pure/Isar/local_theory.ML Wed Dec 27 13:17:55 2023 +0100
@@ -30,7 +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 full_name_pos: 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
@@ -187,7 +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);
+fun full_name_pos 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;