Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed export_standard_morphism;
authorwenzelm
Wed, 29 Nov 2006 15:45:00 +0100
changeset 21593 282c40fb001a
parent 21592 8831206d7f41
child 21594 2859c94d67d4
removed export_standard_morphism;
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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 **)
isabelle