--- 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]},
--- 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]},
--- 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
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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 =
--- 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) =
--- 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 =
--- 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;
--- 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) =
--- 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);
--- 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)));
--- 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
--- 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)
--- 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)
--- 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)
--- 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
--- 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."
--- 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, _), ...} =>
--- 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
--- 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
--- 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
--- 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;
--- 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;
--- 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;
--- 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)
--- 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},
--- 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;
--- 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;
--- 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);
--- 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
--- 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' =
--- 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) =
--- 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;
--- 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);
--- 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;
--- 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 =>
--- 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;
--- 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)
--- 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