# HG changeset patch
# User wenzelm
# Date 1164811500 -3600
# Node ID 282c40fb001aba2eca554a6812d3f3118328d58b
# Parent  8831206d7f419480209cb8597faa76e50953fbbc
removed export_standard_morphism;

diff -r 8831206d7f41 -r 282c40fb001a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Nov 29 15:44:59 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Nov 29 15:45:00 2006 +0100
@@ -73,7 +73,6 @@
   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
@@ -596,10 +595,6 @@
   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 **)