# HG changeset patch
# User wenzelm
# Date 1164560847 -3600
# Node ID 43aa65a8a87029a27eb851a0dbeb361c65897563
# Parent  9e2ff9d4b2b0b3db1e2e58a855b1bd5820750f82
added export_(standard_)morphism;

diff -r 9e2ff9d4b2b0 -r 43aa65a8a870 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 26 18:07:25 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 26 18:07:27 2006 +0100
@@ -72,6 +72,8 @@
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_standard: Proof.context -> Proof.context -> thm list -> thm list
   val standard: Proof.context -> thm list -> thm list
+  val export_morphism: Proof.context -> Proof.context -> morphism
+  val export_standard_morphism: Proof.context -> Proof.context -> morphism
   val add_binds: (indexname * string option) list -> Proof.context -> Proof.context
   val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context
   val auto_bind_goal: term list -> Proof.context -> Proof.context
@@ -573,6 +575,8 @@
 
 (** export theorems **)
 
+(* rules *)
+
 fun common_export is_goal inner outer =
   map (Assumption.export is_goal inner outer) #>
   Variable.export inner outer;
@@ -586,6 +590,17 @@
 fun standard ctxt = export_standard ctxt ctxt;
 
 
+(* morphisms *)
+
+fun export_morphism inner outer =
+  Assumption.export_morphism inner outer $>
+  Variable.export_morphism inner outer;
+
+fun export_standard_morphism inner outer =
+  export_morphism inner outer $>
+  Morphism.thm_morphism Drule.local_standard;
+
+
 
 (** bindings **)