src/Pure/Isar/entity.ML

--- a/src/Pure/Isar/entity.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/entity.ML	Tue May 23 18:46:15 2023 +0200
@@ -35,12 +35,13 @@
 (* local definition *)
 
 fun alias {get_data, put_data} binding name =
-  Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-    let
-      val naming = Name_Space.naming_of context;
-      val binding' = Morphism.binding phi binding;
-      val data' = Name_Space.alias_table naming binding' name (get_data context);
-    in put_data data' context end);
+  Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding}
+    (fn phi => fn context =>
+      let
+        val naming = Name_Space.naming_of context;
+        val binding' = Morphism.binding phi binding;
+        val data' = Name_Space.alias_table naming binding' name (get_data context);
+      in put_data data' context end);
 
 fun transfer {get_data, put_data} ctxt =
   let