# 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'))