# HG changeset patch
# User wenzelm
# Date 1685094411 -7200
# Node ID 10487f6571bc7039c830c9b49ed0dd2dbff44c3b
# Parent  300537844bb7ddf1a63db47f5426198bf9cb7d60
more operations;

diff -r 300537844bb7 -r 10487f6571bc src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Thu May 25 13:58:46 2023 +0200
+++ b/src/Pure/morphism.ML	Fri May 26 11:46:51 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;