clarified treatment of context;

--- a/src/Pure/raw_simplifier.ML	Fri May 26 11:47:45 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Fri May 26 13:19:49 2023 +0200
@@ -38,6 +38,7 @@
   val cert_simproc: theory -> string ->
     {lhss: term list, proc: (Proof.context -> cterm -> thm option) Morphism.entity} -> simproc
   val transform_simproc: morphism -> simproc -> simproc
+  val trim_context_simproc: simproc -> simproc
   val simpset_of: Proof.context -> simpset
   val put_simpset: simpset -> Proof.context -> Proof.context
   val simpset_map: Proof.context -> (Proof.context -> Proof.context) -> simpset -> simpset
@@ -208,7 +209,7 @@
   Proc of
    {name: string,
     lhs: term,
-    proc: Proof.context -> cterm -> thm option,
+    proc: (Proof.context -> cterm -> thm option) Morphism.entity,
     stamp: stamp};
 
 fun eq_proc (Proc {stamp = stamp1, ...}, Proc {stamp = stamp2, ...}) = stamp1 = stamp2;
@@ -721,7 +722,14 @@
   Simproc
    {name = name,
     lhss = map (Morphism.term phi) lhss,
-    proc = Morphism.transform_reset_context phi proc,
+    proc = Morphism.transform phi proc,
+    stamp = stamp};
+
+fun trim_context_simproc (Simproc {name, lhss, proc, stamp}) =
+  Simproc
+   {name = name,
+    lhss = lhss,
+    proc = Morphism.entity_reset_context proc,
     stamp = stamp};
 
 local
@@ -747,7 +755,7 @@
       ctxt);
 
 fun prep_procs (Simproc {name, lhss, proc, stamp}) =
-  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = Morphism.form proc, stamp = stamp});
+  lhss |> map (fn lhs => Proc {name = name, lhs = lhs, proc = proc, stamp = stamp});
 
 in
 
@@ -1041,7 +1049,7 @@
           if Pattern.matches (Proof_Context.theory_of ctxt) (lhs, Thm.term_of t) then
             (cond_tracing' ctxt simp_debug (fn () =>
               print_term ctxt ("Trying procedure " ^ quote name ^ " on:") eta_t);
-             (case proc ctxt eta_t' of
+             (case Morphism.form_context' ctxt proc eta_t' of
                NONE => (cond_tracing' ctxt simp_debug (fn () => "FAILED"); proc_rews ps)
              | SOME raw_thm =>
                  (cond_tracing ctxt (fn () =>

--- a/src/Pure/simplifier.ML	Fri May 26 11:47:45 2023 +0200
+++ b/src/Pure/simplifier.ML	Fri May 26 13:19:49 2023 +0200
@@ -136,14 +136,14 @@
 
 fun def_simproc prep b {lhss, proc} lthy =
   let
-    val simproc =
+    val simproc0 =
       make_simproc lthy (Local_Theory.full_name lthy b) {lhss = prep lthy lhss, proc = proc};
   in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of b}
       (fn phi => fn context =>
         let
           val b' = Morphism.binding phi b;
-          val simproc' = transform_simproc phi simproc;
+          val simproc' = simproc0 |> transform_simproc phi |> trim_context_simproc;
         in
           context
           |> Simprocs.map (#2 o Name_Space.define context true (b', simproc'))