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