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