remove pointless context setup (see also b2e449c155a4);
authorwenzelm
Fri, 19 May 2023 11:42:12 +0200
changeset 78077 5c3e8e6f430a
parent 78076 b2e449c155a4
child 78078 35a86345de48
remove pointless context setup (see also b2e449c155a4);
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'))