# HG changeset patch
# User wenzelm
# Date 1684526946 -7200
# Node ID b0bcba8afdd8ffc94ef80c229c012618238bb9cf
# Parent  270e85124a9a86c6c3c98d1b45de2d0c57d0e2f7
more careful treatment of context for method source;

diff -r 270e85124a9a -r b0bcba8afdd8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri May 19 21:48:11 2023 +0200
+++ b/src/Pure/Isar/method.ML	Fri May 19 22:09:06 2023 +0200
@@ -607,12 +607,17 @@
                   map (fn (a, bs) => (Proof_Context.get_fact ctxt a, map prep_att bs)) xthms;
                 val facts =
                   Attrib.partial_evaluation ctxt [((Binding.name "dummy", []), thms)]
-                  |> map (fn (_, bs) => ((Binding.empty, [Attrib.internal (K attribute)]), bs));
+                  |> map (fn (_, bs) =>
+                    ((Binding.empty, [Attrib.internal (K attribute)]), Attrib.trim_context_thms bs));
 
                 val decl =
-                  Morphism.entity (fn phi =>
-                    Context.mapping I init #>
-                    Attrib.generic_notes "" (Attrib.transform_facts phi facts) #> snd);
+                  Morphism.entity (fn phi => fn context =>
+                    let val psi = Morphism.set_context'' context phi in
+                      context
+                      |> Context.mapping I init
+                      |> Attrib.generic_notes "" (Attrib.transform_facts psi facts)
+                      |> snd
+                    end);
 
                 val modifier_report =
                   (#1 (Token.range_of modifier_toks),