# HG changeset patch
# User wenzelm
# Date 1684259022 -7200
# Node ID a71bfc551891cbf989a7e141187c86a03c3d5d04
# Parent  e6343330e8dfed985548c08cd261358d9ae5111b
more standard treatment of morphism context, but hardly relevant here;

diff -r e6343330e8df -r a71bfc551891 src/Pure/simplifier.ML
--- 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'))