# HG changeset patch # User wenzelm # Date 1164839293 -3600 # Node ID f424d328090c230a0c75c3a0c66c222cb130dbd6 # Parent 2b702007e7c83aaf99c1961f3845974060c89c4a removed export_standard_morphism; Assumption.assms_of: cterm; diff -r 2b702007e7c8 -r f424d328090c src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Nov 29 23:28:11 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Nov 29 23:28:13 2006 +0100 @@ -70,8 +70,6 @@ val read_const: Proof.context -> string -> term val goal_export: Proof.context -> Proof.context -> thm list -> thm list 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 add_binds: (indexname * string option) list -> Proof.context -> Proof.context val add_binds_i: (indexname * term option) list -> Proof.context -> Proof.context @@ -572,9 +570,7 @@ -(** export theorems **) - -(* rules *) +(** export results **) fun common_export is_goal inner outer = map (Assumption.export is_goal inner outer) #> @@ -583,14 +579,6 @@ val goal_export = common_export true; val export = common_export false; -fun export_standard inner outer = - export inner outer #> map Drule.local_standard; - -fun standard ctxt = export_standard ctxt ctxt; - - -(* morphisms *) - fun export_morphism inner outer = Assumption.export_morphism inner outer $> Variable.export_morphism inner outer;