--- a/src/Pure/simplifier.ML Tue May 16 19:42:19 2023 +0200
+++ b/src/Pure/simplifier.ML Tue May 16 19:43:42 2023 +0200
@@ -140,8 +140,9 @@
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
let
- val b' = Morphism.binding phi b;
- val simproc' = transform_simproc phi simproc;
+ val psi = Morphism.set_trim_context'' context phi;
+ val b' = Morphism.binding psi b;
+ val simproc' = transform_simproc psi simproc;
in
context
|> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))