--- a/src/Pure/Isar/bundle.ML Tue May 16 19:52:50 2023 +0200
+++ b/src/Pure/Isar/bundle.ML Tue May 16 20:26:09 2023 +0200
@@ -126,10 +126,13 @@
val bundle =
Attrib.partial_evaluation ctxt' [(Binding.empty_atts, bundle0)]
|> maps #2
- |> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
+ |> transform_bundle (Proof_Context.export_morphism ctxt' lthy)
+ |> trim_context_bundle;
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
+ (fn phi => fn context =>
+ let val psi = Morphism.set_trim_context'' context phi
+ in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end)
end;
in