# HG changeset patch
# User wenzelm
# Date 1726508180 -7200
# Node ID c5ea0cb4dd914838ee40b8ce48766061b66194db
# Parent  c012dfcab50f1993096307ec3886d9c95cacf714
tuned;

diff -r c012dfcab50f -r c5ea0cb4dd91 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Mon Sep 16 18:59:39 2024 +0200
+++ b/src/Pure/Isar/expression.ML	Mon Sep 16 19:36:20 2024 +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 @{here} (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 @{here} (K Locale.witness_add)])])])]
+            [Attrib.internal \<^here> (K Locale.witness_add)])])])]
       else [];
 
     val notes' =