# HG changeset patch
# User wenzelm
# Date 1684577081 -7200
# Node ID 40db83793cea92d5df9bec488c701549e1033b4c
# Parent  b0bcba8afdd8ffc94ef80c229c012618238bb9cf
more operations;

diff -r b0bcba8afdd8 -r 40db83793cea src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Fri May 19 22:09:06 2023 +0200
+++ b/src/Pure/morphism.ML	Sat May 20 12:04:41 2023 +0200
@@ -56,7 +56,9 @@
   val typ_morphism: string -> (typ -> typ) -> morphism
   val term_morphism': string -> (theory -> term -> term) -> morphism
   val term_morphism: string -> (term -> term) -> morphism
+  val fact_morphism': string -> (theory -> thm list -> thm list) -> morphism
   val fact_morphism: string -> (thm list -> thm list) -> morphism
+  val thm_morphism': string -> (theory -> thm -> thm) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
   val transfer_morphism': Proof.context -> morphism
@@ -202,7 +204,9 @@
 fun typ_morphism a typ = morphism a {binding = [], typ = [K typ], term = [], fact = []};
 fun term_morphism' a term = morphism a {binding = [], typ = [], term = [term o the_theory], fact = []};
 fun term_morphism a term = morphism a {binding = [], typ = [], term = [K term], fact = []};
+fun fact_morphism' a fact = morphism a {binding = [], typ = [], term = [], fact = [fact o the_theory]};
 fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [K fact]};
+fun thm_morphism' a thm = morphism a {binding = [], typ = [], term = [], fact = [map o thm o the_theory]};
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [K (map thm)]};
 
 fun transfer_morphism thy = fact_morphism "transfer" I |> set_context thy;