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}