# HG changeset patch
# User wenzelm
# Date 1686043619 -7200
# Node ID db2a6f9aaa779daddf77f43c3238f94be29eb51b
# Parent  a11ebc8c751a432e8af342478199016ceed2baf0
tuned signature: more operations;

diff -r a11ebc8c751a -r db2a6f9aaa77 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jun 06 11:07:49 2023 +0200
+++ b/src/Pure/thm.ML	Tue Jun 06 11:26:59 2023 +0200
@@ -92,7 +92,11 @@
   val trim_context_ctyp: ctyp -> ctyp
   val trim_context_cterm: cterm -> cterm
   val transfer_ctyp: theory -> ctyp -> ctyp
+  val transfer_ctyp': Proof.context -> ctyp -> ctyp
+  val transfer_ctyp'': Context.generic -> ctyp -> ctyp
   val transfer_cterm: theory -> cterm -> cterm
+  val transfer_cterm': Proof.context -> cterm -> cterm
+  val transfer_cterm'': Context.generic -> cterm -> cterm
   val transfer: theory -> thm -> thm
   val transfer': Proof.context -> thm -> thm
   val transfer'': Context.generic -> thm -> thm
@@ -596,6 +600,9 @@
     else Ctyp {cert = cert', T = T, maxidx = maxidx, sorts = sorts}
   end;
 
+val transfer_ctyp' = transfer_ctyp o Proof_Context.theory_of;
+val transfer_ctyp'' = transfer_ctyp o Context.theory_of;
+
 fun transfer_cterm thy' ct =
   let
     val Cterm {cert, t, T, maxidx, sorts} = ct;
@@ -609,6 +616,9 @@
     else Cterm {cert = cert', t = t, T = T, maxidx = maxidx, sorts = sorts}
   end;
 
+val transfer_cterm' = transfer_cterm o Proof_Context.theory_of;
+val transfer_cterm'' = transfer_cterm o Context.theory_of;
+
 fun transfer thy' th =
   let
     val Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) = th;