src/Pure/variable.ML

--- a/src/Pure/variable.ML	Fri Nov 24 22:05:17 2006 +0100
+++ b/src/Pure/variable.ML	Fri Nov 24 22:05:18 2006 +0100
@@ -42,6 +42,7 @@
   val exportT: Proof.context -> Proof.context -> thm list -> thm list
   val export_prf: Proof.context -> Proof.context -> Proofterm.proof -> Proofterm.proof
   val export: Proof.context -> Proof.context -> thm list -> thm list
+  val export_morphism: Proof.context -> Proof.context -> morphism
   val importT_inst: term list -> Proof.context -> ((indexname * sort) * typ) list * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
     (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Proof.context
@@ -203,7 +204,7 @@
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Drule.fold_terms declare_internal;
-fun thm_context th = declare_thm th (Context.init_proof (Thm.theory_of_thm th));
+fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));
 
 
 (* renaming term/type frees *)
@@ -351,6 +352,12 @@
 val exportT = gen_export (rpair [] oo exportT_inst);
 val export = gen_export export_inst;
 
+fun export_morphism inner outer =
+  let
+    val fact = export inner outer;
+    val term = singleton (export_terms inner outer);
+    val typ = Logic.type_map term;
+  in Morphism.morphism {name = I, var = I, typ = typ, term = term, fact = fact} end;
 
 
 (** import -- fix schematic type/term variables **)
@@ -380,7 +387,7 @@
 
 fun importT ths ctxt =
   let
-    val thy = Context.theory_of_proof ctxt;
+    val thy = ProofContext.theory_of ctxt;
     val certT = Thm.ctyp_of thy;
     val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
     val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
@@ -395,7 +402,7 @@
 
 fun import is_open ths ctxt =
   let
-    val thy = Context.theory_of_proof ctxt;
+    val thy = ProofContext.theory_of ctxt;
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
     val ((instT, inst), ctxt') = import_inst is_open (map Thm.full_prop_of ths) ctxt;