# HG changeset patch
# User wenzelm
# Date 1684258939 -7200
# Node ID e6343330e8dfed985548c08cd261358d9ae5111b
# Parent  11d6a1e62841b92d1d7d7bba59d8ea06d2cc1441
tuned;

diff -r 11d6a1e62841 -r e6343330e8df src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Tue May 16 19:20:18 2023 +0200
+++ b/src/Pure/Isar/bundle.ML	Tue May 16 19:42:19 2023 +0200
@@ -124,7 +124,8 @@
     val bundle0 = raw_bundle
       |> map (fn (fact, atts) => (prep_fact ctxt' fact, map (prep_att ctxt') atts));
     val bundle =
-      Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)] |> map snd |> flat
+      Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)]
+      |> maps #2
       |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true}