--- a/src/Pure/Isar/element.ML Tue Dec 16 15:08:08 2008 +0100
+++ b/src/Pure/Isar/element.ML Tue Dec 16 20:18:46 2008 +0100
@@ -78,6 +78,7 @@
val generalize_facts: Proof.context -> Proof.context ->
(Attrib.binding * (thm list * Attrib.src list) list) list ->
(Attrib.binding * (thm list * Attrib.src list) list) list
+ val transfer_morphism: theory -> morphism
val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
end;
@@ -537,6 +538,15 @@
in facts_map (morph_ctxt morphism) facts end;
+(* transfer to theory using closure *)
+
+fun transfer_morphism thy =
+ let val thy_ref = Theory.check_thy thy in
+ Morphism.morphism {binding = I, var = I, typ = I, term = I,
+ fact = map (fn th => transfer (Theory.deref thy_ref) th)}
+ end;
+
+
(** activate in context, return elements and facts **)
local