# HG changeset patch
# User wenzelm
# Date 1441040641 -7200
# Node ID 01b23bfb49478fd0bb57ab7bdf5555e10ec8e6e7
# Parent  d0c21a68d9c6c3b328c6d0f311ffa648113b74b4
tuned signature;

diff -r d0c21a68d9c6 -r 01b23bfb4947 src/Pure/morphism.ML
--- a/src/Pure/morphism.ML	Mon Aug 31 19:02:00 2015 +0200
+++ b/src/Pure/morphism.ML	Mon Aug 31 19:04:01 2015 +0200
@@ -35,6 +35,7 @@
   val fact_morphism: string -> (thm list -> thm list) -> morphism
   val thm_morphism: string -> (thm -> thm) -> morphism
   val transfer_morphism: theory -> morphism
+  val trim_context_morphism: morphism
   val identity: morphism
   val compose: morphism -> morphism -> morphism
   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
@@ -91,6 +92,7 @@
 fun fact_morphism a fact = morphism a {binding = [], typ = [], term = [], fact = [fact]};
 fun thm_morphism a thm = morphism a {binding = [], typ = [], term = [], fact = [map thm]};
 val transfer_morphism = thm_morphism "transfer" o Thm.transfer;
+val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
 
 val identity = morphism "" {binding = [], typ = [], term = [], fact = []};