diff -r 7c9f290dff55 -r 4e865c45458b src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Tue May 16 15:15:56 2023 +0200
+++ b/src/Pure/morphism.ML	Tue May 16 17:08:31 2023 +0200
@@ -53,6 +53,9 @@
   val transfer_morphism': Proof.context -> morphism
   val transfer_morphism'': Context.generic -> morphism
   val trim_context_morphism: morphism
+  val set_trim_context: theory -> morphism -> morphism
+  val set_trim_context': Proof.context -> morphism -> morphism
+  val set_trim_context'': Context.generic -> morphism -> morphism
   val instantiate_frees_morphism: ctyp TFrees.table * cterm Frees.table -> morphism
   val instantiate_morphism: ctyp TVars.table * cterm Vars.table -> morphism
 end;
@@ -183,6 +186,10 @@
 
 val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
+fun set_trim_context thy phi = set_context thy phi $> trim_context_morphism;
+val set_trim_context' = set_trim_context o Proof_Context.theory_of;
+val set_trim_context'' = set_trim_context o Context.theory_of;
+
 
 (* instantiate *)