# HG changeset patch
# User desharna
# Date 1685223282 -7200
# Node ID a8e5cefeb3ab91880d92c5ea62c825cc4d41e51b
# Parent  6f43068a71d158dec1aa5e6f9e7edb6f47be4338# Parent  cc17e2f0f1fcdb8fff39d86224629901527779c2
merged

diff -r 6f43068a71d1 -r a8e5cefeb3ab src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat May 27 23:34:07 2023 +0200
+++ b/src/HOL/Tools/record.ML	Sat May 27 23:34:42 2023 +0200
@@ -1116,9 +1116,8 @@
         | _ => NONE)
       end}));
 
-val simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none);
-val simproc = Simplifier.the_simproc (Context.the_local_context ()) simproc_name;
+val simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("select_update", Position.none));
 
 fun get_upd_acc_cong_thm upd acc thy ss =
   let
@@ -1284,9 +1283,8 @@
         else NONE
       end}));
 
-val upd_simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none);
-val upd_simproc = Simplifier.the_simproc (Context.the_local_context ()) upd_simproc_name;
+val upd_simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("update", Position.none));
 
 end;
 
@@ -1319,8 +1317,9 @@
               | SOME thm => SOME (thm RS @{thm Eq_TrueI})))
       | _ => NONE)}));
 
-val eq_simproc_name = Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none);
-val eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) eq_simproc_name;
+val eq_simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("eq", Position.none));
+
 
 (* split_simproc *)
 
@@ -1398,9 +1397,9 @@
         | _ => NONE)
       end}));
 
-val ex_sel_eq_simproc_name =
-  Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none);
-val ex_sel_eq_simproc = Simplifier.the_simproc (Context.the_local_context ()) ex_sel_eq_simproc_name;
+val ex_sel_eq_simproc =
+  #2 (Simplifier.check_simproc (Context.the_local_context ()) ("ex_sel_eq", Position.none));
+
 val _ = Theory.setup (map_theory_simpset (fn ctxt => ctxt delsimprocs [ex_sel_eq_simproc]));
 
 
diff -r 6f43068a71d1 -r a8e5cefeb3ab src/Pure/ex/Def.thy
--- a/src/Pure/ex/Def.thy	Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/ex/Def.thy	Sat May 27 23:34:42 2023 +0200
@@ -32,6 +32,9 @@
 fun transform_def phi ({lhs, eq}: def) =
   {lhs = Morphism.term phi lhs, eq = Morphism.thm phi eq};
 
+fun trim_context_def ({lhs, eq}: def) =
+  {lhs = lhs, eq = Thm.trim_context eq};
+
 structure Data = Generic_Data
 (
   type T = def Item_Net.T;
@@ -43,8 +46,8 @@
   let val def0: def = {lhs = lhs, eq = Thm.trim_context eq} in
     lthy |> Local_Theory.declaration {syntax = false, pervasive = true, pos = \<^here>}
       (fn phi => fn context =>
-        let val psi = Morphism.set_trim_context'' context phi
-        in (Data.map o Item_Net.update) (transform_def psi def0) context end)
+        let val def' = def0 |> transform_def phi |> trim_context_def
+        in (Data.map o Item_Net.update) def' context end)
   end;
 
 fun get_def ctxt ct =
diff -r 6f43068a71d1 -r a8e5cefeb3ab src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/morphism.ML	Sat May 27 23:34:42 2023 +0200
@@ -49,6 +49,9 @@
   val transform_reset_context: morphism -> 'a entity -> 'a entity
   val form: 'a entity -> 'a
   val form_entity: (morphism -> 'a) -> 'a
+  val form_context: theory -> (theory -> 'a) entity -> 'a
+  val form_context': Proof.context -> (Proof.context -> 'a) entity -> 'a
+  val form_context'': Context.generic -> (Context.generic -> 'a) entity -> 'a
   type declaration = morphism -> Context.generic -> Context.generic
   type declaration_entity = (Context.generic -> Context.generic) entity
   val binding_morphism: string -> (binding -> binding) -> morphism
@@ -193,6 +196,10 @@
 fun form (Entity (f, phi)) = f phi;
 fun form_entity f = f identity;
 
+fun form_context thy x = form (entity_set_context thy x) thy;
+fun form_context' ctxt x = form (entity_set_context' ctxt x) ctxt;
+fun form_context'' context x = form (entity_set_context'' context x) context;
+
 type declaration = morphism -> Context.generic -> Context.generic;
 type declaration_entity = (Context.generic -> Context.generic) entity;
 
diff -r 6f43068a71d1 -r a8e5cefeb3ab src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Sat May 27 23:34:42 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 () =>
diff -r 6f43068a71d1 -r a8e5cefeb3ab src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sat May 27 23:34:07 2023 +0200
+++ b/src/Pure/simplifier.ML	Sat May 27 23:34:42 2023 +0200
@@ -35,7 +35,7 @@
   val simp_flip: attribute
   val cong_add: attribute
   val cong_del: attribute
-  val check_simproc: Proof.context -> xstring * Position.T -> string
+  val check_simproc: Proof.context -> xstring * Position.T -> string * simproc
   val the_simproc: Proof.context -> string -> simproc
   type 'a simproc_spec = {lhss: 'a list, proc: morphism -> Proof.context -> cterm -> thm option}
   val make_simproc: Proof.context -> string -> term simproc_spec -> simproc
@@ -109,14 +109,13 @@
 
 val get_simprocs = Simprocs.get o Context.Proof;
 
-fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt) #> #1;
 val the_simproc = Name_Space.get o get_simprocs;
+fun check_simproc ctxt = Name_Space.check (Context.Proof ctxt) (get_simprocs ctxt);
 
 val _ = Theory.setup
   (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
-    (Args.context -- Scan.lift Parse.embedded_position
-      >> (fn (ctxt, name) =>
-        "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));
+    (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, name) =>
+      "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (#1 (check_simproc ctxt name)))));
 
 
 (* define simprocs *)
@@ -136,14 +135,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'))
@@ -319,7 +318,7 @@
 
 val simproc_att =
   (Args.context -- Scan.lift add_del) :|-- (fn (ctxt, decl) =>
-    Scan.repeat1 (Scan.lift (Args.named_attribute (decl o the_simproc ctxt o check_simproc ctxt))))
+    Scan.repeat1 (Scan.lift (Args.named_attribute (decl o #2 o check_simproc ctxt))))
   >> (fn atts => Thm.declaration_attribute (fn th =>
         fold (fn att => Thm.attribute_declaration (Morphism.form att) th) atts));