# HG changeset patch
# User wenzelm
# Date 1684524159 -7200
# Node ID 35a86345de48f29d9ff49121c5cf2daffb43fdc3
# Parent  5c3e8e6f430a8853e4fe1a4a705d646a48be3061
clarified signature;

diff -r 5c3e8e6f430a -r 35a86345de48 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Fri May 19 11:42:12 2023 +0200
+++ b/src/Pure/morphism.ML	Fri May 19 21:22:39 2023 +0200
@@ -46,6 +46,7 @@
   val entity_set_context': Proof.context -> 'a entity -> 'a entity
   val entity_set_context'': Context.generic -> 'a entity -> 'a entity
   val transform: morphism -> 'a entity -> 'a entity
+  val transform_reset_context: morphism -> 'a entity -> 'a entity
   val form: 'a entity -> 'a
   val form_entity: (morphism -> 'a) -> 'a
   type declaration = (Context.generic -> Context.generic) entity
@@ -185,8 +186,9 @@
 fun entity_set_context'' context a = entity_morphism (set_context'' context) a;
 
 fun transform phi2 (Entity (f, phi1)) = Entity (f, phi1 $> phi2);
+fun transform_reset_context phi2 (Entity (f, phi1)) = Entity (f, reset_context (phi1 $> phi2));
+
 fun form (Entity (f, phi)) = f phi;
-
 fun form_entity f = f identity;
 
 type declaration = (Context.generic -> Context.generic) entity;
diff -r 5c3e8e6f430a -r 35a86345de48 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Fri May 19 11:42:12 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri May 19 21:22:39 2023 +0200
@@ -722,7 +722,7 @@
   Simproc
    {name = name,
     lhss = map (Morphism.term phi) lhss,
-    proc = Morphism.transform phi proc |> Morphism.entity_reset_context,
+    proc = Morphism.transform_reset_context phi proc,
     stamp = stamp};
 
 local