diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue May 16 17:08:31 2023 +0200
@@ -187,12 +187,19 @@
 fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
 
 
-(* fact expressions *)
+(* implicit context *)
+
+val trim_context_binding: Attrib.binding -> Attrib.binding =
+  apsnd ((map o map) Token.trim_context);
 
-val trim_context_binding: Attrib.binding -> Attrib.binding = apsnd (map Token.trim_context_src);
-val trim_context_thms: thms -> thms = (map o apfst o map) Thm.trim_context;
+val trim_context_thms: thms -> thms =
+  map (fn (thms, atts) => (map Thm.trim_context thms, (map o map) Token.trim_context atts));
+
 fun trim_context_fact (binding, thms) = (trim_context_binding binding, trim_context_thms thms);
 
+
+(* fact expressions *)
+
 fun global_notes kind facts thy = thy |>
   Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);