# HG changeset patch
# User wenzelm
# Date 1684860375 -7200
# Node ID bc42c074e58f2a3bf435777ec0447970799425d9
# Parent  c3efa0b63d2e3b202089cfabcc14c84c03a336eb
tuned signature: more position information;

diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Tue May 23 18:46:15 2023 +0200
@@ -943,7 +943,7 @@
 begin
 
 local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false}
+Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
   (fn phi => Ring_Tac.Ring_Simps.map (Ring_Tac.insert_rules Ring_Tac.eq_ring_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms Ipol.simps [meta] Ipol_Pc [meta]},
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Decision_Procs/Reflective_Field.thy
--- a/src/HOL/Decision_Procs/Reflective_Field.thy	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Tue May 23 18:46:15 2023 +0200
@@ -910,7 +910,7 @@
 begin
 
 local_setup \<open>
-Local_Theory.declaration {syntax = false, pervasive = false}
+Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
   (fn phi => Field_Tac.Field_Simps.map (Ring_Tac.insert_rules Field_Tac.eq_field_simps
     (Morphism.term phi \<^term>\<open>R\<close>,
      (Morphism.fact phi @{thms feval.simps [meta] feval_Cnst [meta]},
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Eisbach/Tests.thy
--- a/src/HOL/Eisbach/Tests.thy	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Eisbach/Tests.thy	Tue May 23 18:46:15 2023 +0200
@@ -433,7 +433,7 @@
 begin
 
 local_setup
-  \<open>Local_Theory.declaration {pervasive = false, syntax = false}
+  \<open>Local_Theory.declaration {pervasive = false, syntax = false, pos = \<^here>}
     (fn phi => Data.put (Morphism.fact phi @{thms A}))\<close>
 
 lemma A by dynamic_thms_test
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Tue May 23 18:46:15 2023 +0200
@@ -66,13 +66,14 @@
   let
     val name = Local_Theory.full_name lthy binding;
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
-      Data.map
-        (Symtab.update (name,
-          {vars = map (Morphism.term phi) (#vars closure),
-           named_thms = #named_thms closure,
-           methods = #methods closure,
-           body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding}
+      (fn phi =>
+        Data.map
+          (Symtab.update (name,
+            {vars = map (Morphism.term phi) (#vars closure),
+             named_thms = #named_thms closure,
+             methods = #methods closure,
+             body = (Method.map_source o map) (Token.transform phi) (#body closure)})))
   end;
 
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Tue May 23 18:46:15 2023 +0200
@@ -171,7 +171,7 @@
     fun unfold_note (name, thm) : Attrib.binding * Thm.thm list =
       let
         val thm_name = Binding.qualify true name (Binding.name "unfold")
-        val src = Attrib.internal (K add_unfold)
+        val src = Attrib.internal \<^here> (K add_unfold)
       in
         ((thm_name, [src]), [thm])
       end
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Library/adhoc_overloading.ML
--- a/src/HOL/Library/adhoc_overloading.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML	Tue May 23 18:46:15 2023 +0200
@@ -227,7 +227,7 @@
       |> map (apfst (const_name lthy))
       |> map (apsnd (map (read_term lthy)));
   in
-    Local_Theory.declaration {syntax = true, pervasive = false}
+    Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (adhoc_overloading_cmd' add args) lthy
   end;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue May 23 18:46:15 2023 +0200
@@ -566,7 +566,7 @@
         val strong_cases = map (mk_cases_proof ##> Inductive.rulify lthy1)
           (thsss ~~ elims ~~ cases_prems ~~ cases_prems');
         val strong_induct_atts =
-          map (Attrib.internal o K)
+          map (Attrib.internal \<^here> o K)
             [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
           if length names > 1 then strong_raw_induct
@@ -580,12 +580,12 @@
         Local_Theory.notes
           [((rec_qualified (Binding.name "strong_inducts"), []),
             strong_inducts |> map (fn th => ([th],
-              [Attrib.internal (K ind_case_names),
-               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
+              [Attrib.internal \<^here> (K ind_case_names),
+               Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd |>
         Local_Theory.notes (map (fn ((name, elim), (_, cases)) =>
             ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
-              [Attrib.internal (K (Rule_Cases.case_names (map snd cases))),
-               Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
+              [Attrib.internal \<^here> (K (Rule_Cases.case_names (map snd cases))),
+               Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of elim)))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
@@ -675,7 +675,7 @@
     lthy |>
     Local_Theory.notes (map (fn (name, ths) =>
         ((Binding.qualified_name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
-          [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
+          [Attrib.internal \<^here> (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd
   end;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue May 23 18:46:15 2023 +0200
@@ -466,7 +466,7 @@
         val strong_raw_induct =
           mk_ind_proof lthy1 thss' |> Inductive.rulify lthy1;
         val strong_induct_atts =
-          map (Attrib.internal o K)
+          map (Attrib.internal \<^here> o K)
             [ind_case_names, Rule_Cases.consumes (~ (Thm.nprems_of strong_raw_induct))];
         val strong_induct =
           if length names > 1 then strong_raw_induct
@@ -484,8 +484,8 @@
         lthy2 |>
         Local_Theory.notes [((inducts_name, []),
           strong_inducts |> map (fn th => ([th],
-            [Attrib.internal (K ind_case_names),
-             Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
+            [Attrib.internal \<^here> (K ind_case_names),
+             Attrib.internal \<^here> (K (Rule_Cases.consumes (1 - Thm.nprems_of th)))])))] |> snd
       end)
       (map (map (rulify_term thy #> rpair [])) vc_compat)
   end;
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Real_Asymp/exp_log_expression.ML
--- a/src/HOL/Real_Asymp/exp_log_expression.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Real_Asymp/exp_log_expression.ML	Tue May 23 18:46:15 2023 +0200
@@ -229,7 +229,7 @@
     fun decl phi =
       register_custom' binding (Morphism.term phi pat) expand
   in
-    Local_Theory.declaration {syntax = false, pervasive = false} decl
+    Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding} decl
   end
 
 fun register_custom_from_thm binding thm expand = 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Statespace/state_space.ML	Tue May 23 18:46:15 2023 +0200
@@ -346,7 +346,7 @@
               |> map_distinctthm (K tt');
         in context' end));
 
-    val attr = Attrib.internal type_attr;
+    val attr = Attrib.internal \<^here> type_attr;
 
     val assume =
       ((Binding.name dist_thm_name, [attr]),
@@ -378,7 +378,9 @@
 fun add_declaration name decl thy =
   thy
   |> Named_Target.init [] name
-  |> (fn lthy => Local_Theory.declaration {syntax = true, pervasive = false} (decl lthy) lthy)
+  |> (fn lthy =>
+    Local_Theory.declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
+      (decl lthy) lthy)
   |> Local_Theory.exit_global;
 
 fun parent_components thy (Ts, pname, renaming) =
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue May 23 18:46:15 2023 +0200
@@ -2081,7 +2081,7 @@
 val interpret_bnf = BNF_Plugin.data;
 
 fun register_bnf_raw key bnf =
-  Local_Theory.declaration {syntax = false, pervasive = true}
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
     (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
 
 fun register_bnf plugins key bnf =
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue May 23 18:46:15 2023 +0200
@@ -418,7 +418,7 @@
 
 val register_fp_sugars_raw =
   fold (fn fp_sugar as {T = Type (s, _), ...} =>
-    Local_Theory.declaration {syntax = false, pervasive = true}
+    Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))));
 
 fun register_fp_sugars plugins fp_sugars =
@@ -1069,7 +1069,7 @@
                   |> rotate_prems ~1;
 
                 val cases_set_attr =
-                  Attrib.internal (K (Induct.cases_pred (name_of_set set)));
+                  Attrib.internal \<^here> (K (Induct.cases_pred (name_of_set set)));
 
                 val ctr_names = quasi_unambiguous_case_names (flat
                   (map (uncurry mk_names o map_prod length name_of_ctr) (premss ~~ ctrAs)));
@@ -2031,7 +2031,7 @@
           |> Thm.close_derivation \<^here>;
 
         val case_names_attr = Attrib.case_names (quasi_unambiguous_case_names case_names);
-        val induct_set_attrs = map (Attrib.internal o K o Induct.induct_pred o name_of_set) sets;
+        val induct_set_attrs = map (Attrib.internal \<^here> o K o Induct.induct_pred o name_of_set) sets;
       in
         (thm, case_names_attr :: induct_set_attrs)
       end
@@ -2647,8 +2647,8 @@
         val rec_transfer_thmss =
           map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types);
 
-        val induct_type_attr = Attrib.internal o K o Induct.induct_type;
-        val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
+        val induct_type_attr = Attrib.internal \<^here> o K o Induct.induct_type;
+        val induct_pred_attr = Attrib.internal \<^here> o K o Induct.induct_pred;
 
         val ((rel_induct_thmss, common_rel_induct_thms),
              (rel_induct_attrs, common_rel_induct_attrs)) =
@@ -2808,8 +2808,8 @@
         val corec_code_thms = map (eq_ifIN lthy) corec_thmss;
         val corec_sel_thmss = map flat corec_sel_thmsss;
 
-        val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
-        val coinduct_pred_attr = Attrib.internal o K o Induct.coinduct_pred;
+        val coinduct_type_attr = Attrib.internal \<^here> o K o Induct.coinduct_type;
+        val coinduct_pred_attr = Attrib.internal \<^here> o K o Induct.coinduct_pred;
 
         val flat_corec_thms = append oo append;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue May 23 18:46:15 2023 +0200
@@ -59,7 +59,7 @@
   #> Option.map (transfer_n2m_sugar (Proof_Context.theory_of ctxt));
 
 fun register_n2m_sugar key n2m_sugar =
-  Local_Theory.declaration {syntax = false, pervasive = false}
+  Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
     (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
 
 fun unfold_lets_splits (Const (\<^const_name>\<open>Let\<close>, _) $ t $ u) =
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_gfp_grec.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec.ML	Tue May 23 18:46:15 2023 +0200
@@ -2909,7 +2909,7 @@
   end;
 
 fun set_corec_info_exprs fpT_name f =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()} (fn phi =>
     let val exprs = f phi in
       Data.map (apsnd (fn [info_tab] => [Symtab.map_default (fpT_name, exprs) (K exprs) info_tab]))
     end);
@@ -3214,7 +3214,7 @@
     let
       val (info_tab', lthy) = fold_rev (uncurry o merge_corec_info_tabs) info_tabs (info_tab, lthy);
     in
-      Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+      Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()} (fn phi =>
           Data.map (apsnd (fn _ => [Symtab.map (K (map (morph_corec_info_expr phi))) info_tab'])))
         lthy
     end);
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Tue May 23 18:46:15 2023 +0200
@@ -143,8 +143,9 @@
 );
 
 fun register_codatatype_extra fpT_name extra =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
-    Data.map (@{apply 3(1)} (Symtab.update (fpT_name, morph_codatatype_extra phi extra))));
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+    (fn phi =>
+      Data.map (@{apply 3(1)} (Symtab.update (fpT_name, morph_codatatype_extra phi extra))));
 
 fun codatatype_extra_of ctxt =
   Symtab.lookup (#1 (Data.get (Context.Proof ctxt)))
@@ -154,19 +155,21 @@
   Symtab.dest (#1 (Data.get (Context.Proof ctxt)));
 
 fun register_coinduct_extra fpT_name extra =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
-    Data.map (@{apply 3(2)} (Symtab.update (fpT_name, morph_coinduct_extra phi extra))));
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+    (fn phi =>
+      Data.map (@{apply 3(2)} (Symtab.update (fpT_name, morph_coinduct_extra phi extra))));
 
 fun coinduct_extra_of ctxt =
   Symtab.lookup (#2 (Data.get (Context.Proof ctxt)))
   #> Option.map (transfer_coinduct_extra (Proof_Context.theory_of ctxt));
 
 fun register_friend_extra fun_name eq_algrho algrho_eq =
-  Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
-    Data.map (@{apply 3(3)} (Symtab.map_default (fun_name, empty_friend_extra)
-      (fn {eq_algrhos, algrho_eqs} =>
-        {eq_algrhos = Morphism.thm phi eq_algrho :: eq_algrhos,
-         algrho_eqs = Morphism.thm phi algrho_eq :: algrho_eqs}))));
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = Position.thread_data ()}
+    (fn phi =>
+      Data.map (@{apply 3(3)} (Symtab.map_default (fun_name, empty_friend_extra)
+        (fn {eq_algrhos, algrho_eqs} =>
+          {eq_algrhos = Morphism.thm phi eq_algrho :: eq_algrhos,
+           algrho_eqs = Morphism.thm phi algrho_eq :: algrho_eqs}))));
 
 fun all_friend_extras_of ctxt =
   Symtab.dest (#3 (Data.get (Context.Proof ctxt)));
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue May 23 18:46:15 2023 +0200
@@ -382,7 +382,7 @@
       val phi0 = substitute_noted_thm noted;
     in
       lthy3
-      |> Local_Theory.declaration {syntax = false, pervasive = true}
+      |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi => Data.map (@{fold 3} (fn T_name => fn Const (size_name, _) =>
             fn overloaded_size_def =>
                let val morph = Morphism.thm (phi0 $> phi) in
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue May 23 18:46:15 2023 +0200
@@ -210,7 +210,7 @@
 val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
 
 fun register_ctr_sugar_raw (ctr_sugar as {T = Type (name, _), ...}) =
-  Local_Theory.declaration {syntax = false, pervasive = true}
+  Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
     (fn phi => fn context =>
       let val pos = Position.thread_data ()
       in Data.map (Symtab.update (name, (pos, morph_ctr_sugar phi ctr_sugar))) context end);
@@ -1072,8 +1072,8 @@
             |> Thm.close_derivation \<^here>
           end;
 
-        val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
-        val cases_type_attr = Attrib.internal (K (Induct.cases_type fcT_name));
+        val exhaust_case_names_attr = Attrib.internal \<^here> (K (Rule_Cases.case_names exhaust_cases));
+        val cases_type_attr = Attrib.internal \<^here> (K (Induct.cases_type fcT_name));
 
         val nontriv_disc_eq_thmss =
           map (map (fn th => th RS @{thm eq_False[THEN iffD2]}
@@ -1119,12 +1119,12 @@
             (AList.group (eq_list (op aconv)) (map (`(single o lhs_head_of)) all_sel_thms))
           |> fold (uncurry (Spec_Rules.add Binding.empty Spec_Rules.equational))
             (filter_out (null o snd) (map single discs ~~ nontriv_disc_eq_thmss))
-          |> Local_Theory.declaration {syntax = false, pervasive = true}
+          |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
             (fn phi => Case_Translation.register
                (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
           |> plugins code_plugin ?
              (Code.declare_default_eqns (map (rpair true) (flat nontriv_disc_eq_thmss @ case_thms @ all_sel_thms))
-             #> Local_Theory.declaration {syntax = false, pervasive = false}
+             #> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
                (fn phi => Context.mapping
                   (add_ctr_code fcT_name (map (Morphism.typ phi) As)
                      (map (dest_Const o Morphism.term phi) ctrs) (Morphism.fact phi inject_thms)
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Function/function.ML	Tue May 23 18:46:15 2023 +0200
@@ -129,7 +129,7 @@
             (K false) (map fst fixes)
       in
         (info,
-         lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false}
+         lthy2 |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
           (fn phi => add_function_data (transform_function_data phi info)))
       end
   in
@@ -209,7 +209,7 @@
           in
             (info',
              lthy2
-             |> Local_Theory.declaration {syntax = false, pervasive = false}
+             |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
                (fn phi => add_function_data (transform_function_data phi info'))
              |> Spec_Rules.add Binding.empty Spec_Rules.equational_recdef fs tsimps)
           end)
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Lifting/lifting_def.ML
--- a/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Tue May 23 18:46:15 2023 +0200
@@ -528,7 +528,7 @@
 
   val register_code_eq_attribute = Thm.declaration_attribute
     (fn thm => Context.mapping (register_encoded_code_eq thm) I)
-  val register_code_eq_attrib = Attrib.internal (K register_code_eq_attribute)
+  val register_code_eq_attrib = Attrib.internal \<^here> (K register_code_eq_attribute)
 
 in
 
@@ -547,7 +547,7 @@
             which code equation is going to be used. This is going to be resolved at the
             point when an interpretation of the locale is executed. *)
         val lthy'' = lthy'
-          |> Local_Theory.declaration {syntax = false, pervasive = true} (K (Data.put NONE))
+          |> Local_Theory.declaration {syntax = false, pervasive = true, pos =  \<^here>} (K (Data.put NONE))
       in (code_eq, lthy'') end
     else
       (NONE_EQ, lthy)
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Tue May 23 18:46:15 2023 +0200
@@ -146,7 +146,7 @@
 
 fun update_code_dt code_dt =
   (snd o Local_Theory.begin_nested)
-  #> Local_Theory.declaration {syntax = false, pervasive = true}
+  #> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
     (fn phi => Data.map (Item_Net.update (morph_code_dt phi code_dt)))
   #> Local_Theory.end_nested
 
@@ -346,7 +346,7 @@
       |> update_rep_isom rep_isom (transfer_rules_of_lift_def rep_isom_lift_def |> hd)
           (bundle_name_of_bundle_binding qty_isom_bundle phi context) pointer;
     val lthy3 = lthy2  
-      |> Local_Theory.declaration {syntax = false, pervasive = true}
+      |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi => fn context => Data.map (Item_Net.update (morph_code_dt phi (code_dt phi context))) context)
       |> Local_Theory.end_nested
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Tue May 23 18:46:15 2023 +0200
@@ -248,7 +248,7 @@
       ([dummy_thm], [map Token.make_string0 ["Lifting.lifting_restore_internal", bundle_name]])
   in
     lthy
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
+    |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi => Lifting_Info.init_restore_data bundle_name (phi_qinfo phi))
     |> Bundle.bundle ((binding, [restore_lifting_att])) []
     |> pair binding
@@ -272,7 +272,7 @@
     val quotients = { quot_thm = quot_thm, pcr_info = pcr_info }
     val qty_full_name = (fst o dest_Type) qty
     fun quot_info phi = Lifting_Info.transform_quotient phi quotients
-    val reflexivity_rule_attr = Attrib.internal (K Lifting_Info.add_reflexivity_rule_attribute)
+    val reflexivity_rule_attr = Attrib.internal \<^here> (K Lifting_Info.add_reflexivity_rule_attribute)
     val lthy3 =
       case opt_reflp_thm of
         SOME reflp_thm =>
@@ -283,7 +283,7 @@
       | NONE => lthy2 |> define_abs_type quot_thm
   in
     lthy3
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
+    |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi => Lifting_Info.update_quotients qty_full_name (quot_info phi))
     |> lifting_bundle qty_full_name quotients
   end
@@ -520,7 +520,7 @@
     val quot_thm = Morphism.thm (Local_Theory.target_morphism lthy0) quot_thm
     (**)
     val (rty, qty) = quot_thm_rty_qty quot_thm
-    val induct_attr = Attrib.internal (K (Induct.induct_type (fst (dest_Type qty))))
+    val induct_attr = Attrib.internal \<^here> (K (Induct.induct_type (fst (dest_Type qty))))
     val qty_full_name = (fst o dest_Type) qty
     val qty_name = (Binding.name o Long_Name.base_name) qty_full_name
     val qualify = Binding.qualify_name true qty_name
@@ -997,7 +997,7 @@
           val quot_thm = #quot_thm qinfo
           val transfer_rules = get_transfer_rules_to_delete qinfo lthy
         in
-          Local_Theory.declaration {syntax = false, pervasive = true}
+          Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
             (K (fold (Transfer.transfer_raw_del) transfer_rules #> Lifting_Info.delete_quotients quot_thm))
             lthy
         end
@@ -1029,7 +1029,7 @@
   in
     case Lifting_Info.lookup_restore_data lthy pointer of
       SOME refresh_data => 
-        Local_Theory.declaration {syntax = false, pervasive = true}
+        Local_Theory.declaration {syntax = false, pervasive = true, pos =  \<^here>}
           (fn phi => Lifting_Info.add_transfer_rules_in_restore_data pointer 
             (new_transfer_rules refresh_data lthy phi)) lthy
     | NONE => error "The lifting bundle refers to non-existent restore data."
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Quotient/quotient_def.ML
--- a/src/HOL/Tools/Quotient/quotient_def.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML	Tue May 23 18:46:15 2023 +0200
@@ -74,7 +74,7 @@
     val rsp_thm_name = qualify lhs_name "rsp"
 
     val lthy'' = lthy'
-      |> Local_Theory.declaration {syntax = false, pervasive = true}
+      |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
         (fn phi =>
           (case qconst_data phi of
             qcinfo as {qconst = Const (c, _), ...} =>
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Quotient/quotient_type.ML
--- a/src/HOL/Tools/Quotient/quotient_type.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML	Tue May 23 18:46:15 2023 +0200
@@ -149,7 +149,7 @@
       Quotient_Info.transform_abs_rep phi {abs = abs, rep = rep}
   in
     lthy
-    |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi =>
+    |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>} (fn phi =>
         Quotient_Info.update_quotients (qty_full_name, quotients phi) #>
         Quotient_Info.update_abs_rep (qty_full_name, abs_rep phi))
     |> setup_lifting_package quot_thm equiv_thm opt_par_thm
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/Transfer/transfer_bnf.ML
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Tue May 23 18:46:15 2023 +0200
@@ -208,7 +208,7 @@
     lthy
     |> Local_Theory.notes notes
     |> snd
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
+    |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
   end
 
@@ -260,7 +260,7 @@
       |> Transfer.update_pred_simps pred_injects
   in
     lthy
-    |> Local_Theory.declaration {syntax = false, pervasive = true}
+    |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data))
   end
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/functor.ML
--- a/src/HOL/Tools/functor.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/functor.ML	Tue May 23 18:46:15 2023 +0200
@@ -263,7 +263,7 @@
         |> Local_Theory.note ((qualify identityN, []),
             [prove_identity lthy id_thm])
         |> snd
-        |> Local_Theory.declaration {syntax = false, pervasive = false}
+        |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
           (mapper_declaration comp_thm id_thm))
   in
     lthy
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/inductive.ML	Tue May 23 18:46:15 2023 +0200
@@ -1032,7 +1032,7 @@
           [Attrib.case_names [rec_name],
            Attrib.case_conclusion (rec_name, intr_names),
            Attrib.consumes (1 - Thm.nprems_of raw_induct),
-           Attrib.internal (K (Induct.coinduct_pred (hd cnames)))])
+           Attrib.internal \<^here> (K (Induct.coinduct_pred (hd cnames)))])
       else if no_ind orelse length cnames > 1 then
         (raw_induct, ind_case_names @ [Attrib.consumes (~ (Thm.nprems_of raw_induct))])
       else
@@ -1055,7 +1055,7 @@
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "cases"),
             ((if forall (equal "") cases then [] else [Attrib.case_names cases]) @
               [Attrib.consumes (1 - Thm.nprems_of elim), Attrib.constraints k,
-               Attrib.internal (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})),
+               Attrib.internal \<^here> (K (Induct.cases_pred name))] @ @{attributes [Pure.elim?]})),
             [elim]) #>
         apfst (hd o snd)) (if null elims then [] else cnames ~~ elims) ||>>
       Local_Theory.note
@@ -1065,7 +1065,7 @@
     val (eqs', lthy3) = lthy2 |>
       fold_map (fn (name, eq) => Local_Theory.note
           ((Binding.qualify true (Long_Name.base_name name) (Binding.name "simps"),
-            [Attrib.internal (K equation_add_permissive)]), [eq])
+            [Attrib.internal \<^here> (K equation_add_permissive)]), [eq])
           #> apfst (hd o snd))
         (if null eqs then [] else (cnames ~~ eqs))
     val (inducts, lthy4) =
@@ -1077,7 +1077,7 @@
             inducts |> map (fn (name, th) => ([th],
               ind_case_names @
                 [Attrib.consumes (1 - Thm.nprems_of th),
-                 Attrib.internal (K (Induct.induct_pred name))])))] |>> snd o hd
+                 Attrib.internal \<^here> (K (Induct.induct_pred name))])))] |>> snd o hd
         end;
   in (intrs', elims', eqs', induct', inducts, lthy4) end;
 
@@ -1144,7 +1144,7 @@
        eqs = eqs'};
 
     val lthy4 = lthy3
-      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
+      |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi =>
         let val result' = transform_result phi result;
         in put_inductives ({names = cnames, coind = coind}, result') end);
   in (result, lthy4) end;
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/inductive_set.ML	Tue May 23 18:46:15 2023 +0200
@@ -494,7 +494,7 @@
                 [def, @{thm mem_Collect_eq}, @{thm case_prod_conv}]) 1))
         in
           lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
-            [Attrib.internal (K pred_set_conv_att)]),
+            [Attrib.internal \<^here> (K pred_set_conv_att)]),
               [conv_thm]) |> snd
         end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/semiring_normalizer.ML
--- a/src/HOL/Tools/semiring_normalizer.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/semiring_normalizer.ML	Tue May 23 18:46:15 2023 +0200
@@ -173,7 +173,7 @@
     val raw_ring = prepare_ops raw_ring0;
     val raw_field = prepare_ops raw_field0;
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn phi => fn context =>
       let
         val ctxt = Context.proof_of context;
         val key = Morphism.thm phi raw_key;
diff -r c3efa0b63d2e -r bc42c074e58f src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/HOL/Tools/typedef.ML	Tue May 23 18:46:15 2023 +0200
@@ -259,19 +259,19 @@
               make @{thm type_definition.Abs_inject})
           ||>> note ((Binding.suffix_name "_cases" Rep_name,
                 [Attrib.case_names [Binding.name_of Rep_name],
-                 Attrib.internal (K (Induct.cases_pred full_name))]),
+                 Attrib.internal \<^here> (K (Induct.cases_pred full_name))]),
               make @{thm type_definition.Rep_cases})
           ||>> note ((Binding.suffix_name "_cases" Abs_name,
                 [Attrib.case_names [Binding.name_of Abs_name],
-                 Attrib.internal (K (Induct.cases_type full_name))]),
+                 Attrib.internal \<^here> (K (Induct.cases_type full_name))]),
               make @{thm type_definition.Abs_cases})
           ||>> note ((Binding.suffix_name "_induct" Rep_name,
                 [Attrib.case_names [Binding.name_of Rep_name],
-                 Attrib.internal (K (Induct.induct_pred full_name))]),
+                 Attrib.internal \<^here> (K (Induct.induct_pred full_name))]),
               make @{thm type_definition.Rep_induct})
           ||>> note ((Binding.suffix_name "_induct" Abs_name,
                 [Attrib.case_names [Binding.name_of Abs_name],
-                 Attrib.internal (K (Induct.induct_type full_name))]),
+                 Attrib.internal \<^here> (K (Induct.induct_type full_name))]),
               make @{thm type_definition.Abs_induct});
 
         val info =
@@ -283,7 +283,7 @@
           Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
       in
         lthy3
-        |> Local_Theory.declaration {syntax = false, pervasive = true}
+        |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
           (fn phi => put_info full_name (transform_info phi info))
         |> Typedef_Plugin.data Plugin_Name.default_filter full_name
         |> pair (full_name, info)
diff -r c3efa0b63d2e -r bc42c074e58f src/Provers/order_tac.ML
--- a/src/Provers/order_tac.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Provers/order_tac.ML	Tue May 23 18:46:15 2023 +0200
@@ -368,15 +368,16 @@
   )
 
   fun declare (octxt as {kind = kind, raw_proc = raw_proc, ...}) lthy =
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-      let
-        val ops = map (Morphism.term phi) (#ops octxt)
-        val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
-        val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
-        val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
-      in
-        context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
-      end)
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>}
+      (fn phi => fn context =>
+        let
+          val ops = map (Morphism.term phi) (#ops octxt)
+          val thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#thms octxt)
+          val conv_thms = map (fn (s, thm) => (s, Morphism.thm phi thm)) (#conv_thms octxt)
+          val octxt' = {kind = kind, ops = ops, thms = thms, conv_thms = conv_thms}
+        in
+          context |> Data.map (Library.insert order_data_eq (octxt', raw_proc))
+        end)
 
   fun declare_order {
       ops = {eq = eq, le = le, lt = lt},
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 23 18:46:15 2023 +0200
@@ -48,8 +48,8 @@
     local_theory -> local_theory
   val attribute_setup: bstring * Position.T -> Input.source -> string ->
     local_theory -> local_theory
-  val internal: (morphism -> attribute) -> Token.src
-  val internal_declaration: Morphism.declaration_entity -> thms
+  val internal: Position.T -> (morphism -> attribute) -> Token.src
+  val internal_declaration: Position.T -> Morphism.declaration_entity -> thms
   val add_del: attribute -> attribute -> attribute context_parser
   val thm: thm context_parser
   val thms: thm list context_parser
@@ -251,13 +251,15 @@
     "internal attribute");
 
 val internal_name = make_name (Context.the_local_context ()) (Binding.name_of internal_binding);
-val internal_arg = Token.make_string0 "<attribute>";
-fun internal_source value = [internal_name, Token.assign (SOME value) internal_arg];
+fun internal_source name value = [internal_name, Token.assign (SOME value) (Token.make_string name)];
 
 in
 
-fun internal arg = internal_source (Token.Attribute (Morphism.entity arg));
-fun internal_declaration arg = [([Drule.dummy_thm], [internal_source (Token.Declaration arg)])];
+fun internal pos arg =
+  internal_source ("<attribute>", pos) (Token.Attribute (Morphism.entity arg));
+
+fun internal_declaration pos arg =
+  [([Drule.dummy_thm], [internal_source ("<declaration>", pos) (Token.Declaration arg)])];
 
 end;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue May 23 18:46:15 2023 +0200
@@ -129,7 +129,7 @@
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy)
       |> trim_context_bundle;
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of binding}
       (fn phi => fn context =>
         let val psi = Morphism.set_trim_context'' context phi
         in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
@@ -181,9 +181,9 @@
     |> Attrib.local_notes kind facts
   end;
 
-fun bundle_declaration decl lthy =
+fun bundle_declaration pos decl lthy =
   lthy
-  |> (augment_target o Attrib.internal_declaration)
+  |> (augment_target o Attrib.internal_declaration pos)
     (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
   |> Generic_Target.standard_declaration (K true) decl;
 
@@ -198,10 +198,10 @@
      {define = bad_operation,
       notes = bundle_notes,
       abbrev = bad_operation,
-      declaration = K bundle_declaration,
+      declaration = fn {pos, ...} => bundle_declaration pos,
       theory_registration = bad_operation,
       locale_dependency = bad_operation,
-      pretty = pretty binding}
+      pretty = pretty binding};
 
 end;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/code.ML	Tue May 23 18:46:15 2023 +0200
@@ -1310,7 +1310,7 @@
 (* abstract code declarations *)
 
 fun code_declaration strictness lift_phi f x =
-  Local_Theory.declaration {syntax = false, pervasive = false}
+  Local_Theory.declaration {syntax = false, pervasive = false, pos = Position.thread_data ()}
     (fn phi => Context.mapping (f strictness (lift_phi phi x)) I);
 
 
diff -r c3efa0b63d2e -r bc42c074e58f 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
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/expression.ML	Tue May 23 18:46:15 2023 +0200
@@ -794,7 +794,7 @@
 fun defines_to_notes ctxt (Defines defs) =
       Notes ("", map (fn (a, (def, _)) =>
         (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)],
-          [Attrib.internal (K Locale.witness_add)])])) defs)
+          [Attrib.internal @{here} (K Locale.witness_add)])])) defs)
   | defines_to_notes _ e = e;
 
 val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false;
@@ -846,7 +846,7 @@
       if is_some asm then
         [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []),
           [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
-            [Attrib.internal (K Locale.witness_add)])])])]
+            [Attrib.internal @{here} (K Locale.witness_add)])])])]
       else [];
 
     val notes' =
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/generic_target.ML	Tue May 23 18:46:15 2023 +0200
@@ -63,16 +63,16 @@
     local_theory -> local_theory
   val locale_target_abbrev: string -> Syntax.mode ->
     (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory
-  val locale_target_declaration: string -> bool -> Morphism.declaration_entity ->
-    local_theory -> local_theory
+  val locale_target_declaration: string -> {syntax: bool, pos: Position.T} ->
+    Morphism.declaration_entity -> local_theory -> local_theory
   val locale_target_const: string -> (morphism -> bool) -> Syntax.mode ->
     (binding * mixfix) * term -> local_theory -> local_theory
 
   (*locale operations*)
   val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> (term * term) * local_theory
-  val locale_declaration: string -> {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
-    local_theory -> local_theory
+  val locale_declaration: string -> {syntax: bool, pervasive: bool, pos: Position.T} ->
+    Morphism.declaration_entity -> local_theory -> local_theory
   val locale_const: string -> Syntax.mode -> (binding * mixfix) * term ->
     local_theory -> local_theory
   val locale_dependency: string -> Locale.registration ->
@@ -443,20 +443,21 @@
       Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #>
   standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts;
 
-fun locale_target_declaration locale syntax decl lthy = lthy
+fun locale_target_declaration locale params decl lthy = lthy
   |> Local_Theory.target (fn ctxt => ctxt |>
-    Locale.add_declaration locale syntax
+    Locale.add_declaration locale params
       (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl));
 
 fun locale_target_const locale phi_pred prmode ((b, mx), rhs) =
-  locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs))
+  locale_target_declaration locale {syntax = true, pos = Binding.pos_of b}
+    (const_decl phi_pred prmode ((b, mx), rhs));
 
 
 (** locale operations **)
 
-fun locale_declaration locale {syntax, pervasive} decl =
+fun locale_declaration locale {syntax, pervasive, pos} decl =
   pervasive ? background_declaration decl
-  #> locale_target_declaration locale syntax decl
+  #> locale_target_declaration locale {syntax = syntax, pos = pos} decl
   #> standard_declaration (fn (_, other) => other <> 0) decl;
 
 fun locale_const locale prmode ((b, mx), rhs) =
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue May 23 18:46:15 2023 +0200
@@ -130,7 +130,8 @@
   ML_Context.expression (Input.pos_of source)
     (ML_Lex.read
       ("Theory.local_setup (Local_Theory.declaration {syntax = " ^
-        Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^ "} (") @
+        Bool.toString syntax ^ ", pervasive = " ^ Bool.toString pervasive ^
+        ", pos = " ^ ML_Syntax.print_position (Position.thread_data ()) ^ "} (") @
      ML_Lex.read_source source @ ML_Lex.read "))")
   |> Context.proof_map;
 
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Tue May 23 18:46:15 2023 +0200
@@ -55,7 +55,7 @@
     (string * thm list) list * local_theory
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
-  val declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration ->
+  val declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration ->
     local_theory -> local_theory
   val theory_registration: Locale.registration -> local_theory -> local_theory
   val locale_dependency: Locale.registration -> local_theory -> local_theory
@@ -103,7 +103,7 @@
   notes: string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory,
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
-  declaration: {syntax: bool, pervasive: bool} -> Morphism.declaration_entity ->
+  declaration: {syntax: bool, pervasive: bool, pos: Position.T} -> Morphism.declaration_entity ->
     local_theory -> local_theory,
   theory_registration: Locale.registration -> local_theory -> local_theory,
   locale_dependency: Locale.registration -> local_theory -> local_theory,
@@ -301,7 +301,7 @@
   |-> (fn name =>
     map_contexts (fn _ => fn ctxt =>
       Proof_Context.transfer_facts (Proof_Context.theory_of ctxt) ctxt) #>
-    declaration {syntax = false, pervasive = false} (fn phi =>
+    declaration {syntax = false, pervasive = false, pos = Binding.pos_of binding} (fn phi =>
       let val binding' = Morphism.binding phi binding in
         Context.mapping
           (Global_Theory.alias_fact binding' name)
@@ -312,7 +312,7 @@
 (* default sort *)
 
 fun set_defsort S =
-  declaration {syntax = true, pervasive = false}
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
@@ -324,7 +324,7 @@
     val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (fn _ => Proof_Context.generic_syntax add mode args') lthy
   end;
 
@@ -343,7 +343,7 @@
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
@@ -354,7 +354,7 @@
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
-    declaration {syntax = true, pervasive = false}
+    declaration {syntax = true, pervasive = false, pos = Position.thread_data ()}
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
@@ -373,7 +373,7 @@
 (* name space aliases *)
 
 fun syntax_alias global_alias local_alias b name =
-  declaration {syntax = true, pervasive = false} (fn phi =>
+  declaration {syntax = true, pervasive = false, pos = Position.thread_data ()} (fn phi =>
     let val b' = Morphism.binding phi b
     in Context.mapping (global_alias b' name) (local_alias b' name) end);
 
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Tue May 23 18:46:15 2023 +0200
@@ -59,7 +59,8 @@
 
   (* Storing results *)
   val add_facts: string -> string -> Attrib.fact list -> Proof.context -> Proof.context
-  val add_declaration: string -> bool -> Morphism.declaration_entity -> Proof.context -> Proof.context
+  val add_declaration: string -> {syntax: bool, pos: Position.T} ->
+    Morphism.declaration_entity -> Proof.context -> Proof.context
 
   (* Activation *)
   val activate_facts: morphism option -> string * morphism -> Context.generic -> Context.generic
@@ -674,11 +675,11 @@
         ((change_locale loc o apfst o apsnd) (cons stored_notes) #> apply_registrations)
     end;
 
-fun add_declaration loc syntax decl =
+fun add_declaration loc {syntax, pos} decl =
   let val decl0 = Morphism.entity_reset_context decl in
     syntax ?
       Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl0, serial ())))
-    #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration decl0)]
+    #> add_facts loc "" [(Binding.empty_atts, Attrib.internal_declaration pos decl0)]
   end;
 
 
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/method.ML	Tue May 23 18:46:15 2023 +0200
@@ -608,7 +608,8 @@
                 val facts =
                   Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
                   |> map (fn (_, bs) =>
-                    ((Binding.empty, [Attrib.internal (K attribute)]), Attrib.trim_context_thms bs));
+                    ((Binding.empty, [Attrib.internal pos (K attribute)]),
+                      Attrib.trim_context_thms bs));
 
                 val decl =
                   Morphism.entity (fn phi => fn context =>
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/Isar/spec_rules.ML	Tue May 23 18:46:15 2023 +0200
@@ -162,7 +162,7 @@
     val n = length terms;
     val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules);
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = Binding.pos_of b}
       (fn phi => fn context =>
         let
           val psi = Morphism.set_trim_context'' context phi;
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/ex/Def.thy	Tue May 23 18:46:15 2023 +0200
@@ -41,7 +41,7 @@
 
 fun declare_def lhs eq lthy =
   let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => fn context =>
         let val psi = Morphism.set_trim_context'' context phi
         in (Data.map o Item_Net.update) (transform_def psi def0) context end)
diff -r c3efa0b63d2e -r bc42c074e58f src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Tue May 23 10:56:41 2023 +0200
+++ b/src/Pure/simplifier.ML	Tue May 23 18:46:15 2023 +0200
@@ -139,15 +139,16 @@
     val simproc =
       make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
   in
-    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
-      let
-        val b' = Morphism.binding phi b;
-        val simproc' = transform_simproc phi simproc;
-      in
-        context
-        |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
-        |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
-      end)
+    lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b}
+      (fn phi => fn context =>
+        let
+          val b' = Morphism.binding phi b;
+          val simproc' = transform_simproc phi simproc;
+        in
+          context
+          |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))
+          |> map_ss (fn ctxt => ctxt addsimprocs [simproc'])
+        end)
   end;
 
 in