# HG changeset patch
# User wenzelm
# Date 1164402313 -3600
# Node ID b165c91207025e6a6c40c26f8d71207bcd4ab6c9
# Parent  c2a116a2c4fdf59128e3fd81b6d952da946e7594
added export_morphism;

diff -r c2a116a2c4fd -r b165c9120702 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Fri Nov 24 22:05:12 2006 +0100
+++ b/src/Pure/assumption.ML	Fri Nov 24 22:05:13 2006 +0100
@@ -18,6 +18,7 @@
   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
   val add_view: Proof.context -> cterm list -> Proof.context -> Proof.context
   val export: bool -> Proof.context -> Proof.context -> thm -> thm
+  val export_morphism: Proof.context -> Proof.context -> morphism
 end;
 
 structure Assumption: ASSUMPTION =
@@ -104,4 +105,11 @@
     #> norm_hhf_protect
   end;
 
+fun export_morphism inner outer =
+  let
+    val thm = export false inner outer;
+    fun term t = Drule.term_rule (ProofContext.theory_of inner (*delayed until now*)) thm t;
+    val typ = Logic.type_map term;
+  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = map thm} end;
+
 end;