# HG changeset patch
# User wenzelm
# Date 1684489332 -7200
# Node ID 5c3e8e6f430a8853e4fe1a4a705d646a48be3061
# Parent  b2e449c155a44cf528a6c03f516e906636f6e843
remove pointless context setup (see also b2e449c155a4);

diff -r b2e449c155a4 -r 5c3e8e6f430a src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Fri May 19 11:41:30 2023 +0200
+++ b/src/Pure/simplifier.ML	Fri May 19 11:42:12 2023 +0200
@@ -141,9 +141,8 @@
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
       let
-        val psi = Morphism.set_trim_context'' context phi;
-        val b' = Morphism.binding psi b;
-        val simproc' = transform_simproc psi simproc;
+        val b' = Morphism.binding phi b;
+        val simproc' = transform_simproc phi simproc;
       in
         context
         |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))