Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
authorwenzelm
Mon, 15 May 2023 22:46:04 +0200
changeset 78061 5ab5add88922
parent 78060 b6c886b7184f
child 78062 edb195122938
proper transfer to supported "bundle ... begin unbundle ... end", e.g. see theory "AFP/Probabilistic_Timed_Automata.Graphs";
src/Pure/Isar/bundle.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle