--- 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' =