--- 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 **)