# HG changeset patch
# User wenzelm
# Date 1684145687 -7200
# Node ID c8c084bd7e1275bd5ee41c8c0373942dc7112376
# Parent  78deba4fdf27a92314a0579c1bb06fbabab24227
proper trim_context / transfer;

diff -r 78deba4fdf27 -r c8c084bd7e12 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon May 15 10:59:49 2023 +0200
+++ b/src/Pure/Isar/interpretation.ML	Mon May 15 12:14:47 2023 +0200
@@ -104,9 +104,12 @@
       fold_map (fn facts => note Thm.theoremK facts #-> abs_def_rule) factss ctxt;
     val defs = (Binding.empty_atts, [(map (Morphism.thm (export' $> export)) def_eqns, [])]);
     val (eqns', ctxt'') = ctxt' |> note Thm.theoremK [defs] |-> abs_def_rule;
+    val transform_witness =
+      Element.transform_witness
+        (Morphism.transfer_morphism' ctxt' $> export' $> Morphism.trim_context_morphism);
     val deps' =
       (deps ~~ witss) |> map (fn ((dep, morph), wits) =>
-        (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits)));
+        (dep, morph $> Element.satisfy_morphism (map transform_witness wits)));
     fun register (dep, eqns) ctxt =
       ctxt |> add_registration
         {inst = dep,