added export_morphism;

--- 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;