# HG changeset patch
# User wenzelm
# Date 1684183564 -7200
# Node ID 5ab5add889229b7545f8f462195f91a3b8ef4e4f
# Parent  b6c886b7184f443b1a9ad8fe5eccaff80e93ec57
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";

diff -r b6c886b7184f -r 5ab5add88922 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Mon May 15 20:55:17 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Mon May 15 22:46:04 2023 +0200
@@ -203,7 +203,7 @@
   let val decls = maps (prep_bundle ctxt) args in
     ctxt
     |> Context_Position.set_visible false
-    |> notes [(Binding.empty_atts, decls)] |> #2
+    |> notes [(Binding.empty_atts, transform_bundle (Morphism.transfer_morphism' ctxt) decls)] |> #2
     |> Context_Position.restore_visible ctxt
   end;