# HG changeset patch
# User wenzelm
# Date 1003857271 -7200
# Node ID 3a4b3c311a978e1ee82a15fdc854e79f42f4f2f9
# Parent  938dd8bca66184c12c1bed123b663d95836fe4dc
removed obsolete "exported" att;

diff -r 938dd8bca661 -r 3a4b3c311a97 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Oct 23 19:14:13 2001 +0200
+++ b/src/Pure/Isar/attrib.ML	Tue Oct 23 19:14:31 2001 +0200
@@ -295,9 +295,6 @@
 fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
 fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
 
-fun exported_global x = no_args (Drule.rule_attribute (Proof.export_thm o ProofContext.init)) x;
-fun exported_local x = no_args (Drule.rule_attribute Proof.export_thm) x;
-
 
 
 (** theory setup **)
@@ -320,7 +317,6 @@
   ("consumes", (consumes, consumes), "number of consumed facts"),
   ("case_names", (case_names, case_names), "named rule cases"),
   ("params", (params, params), "named rule parameters"),
-  ("exported", (exported_global, exported_local), "theorem exported from context"),
   ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute),
     "declaration of atomize rule"),
   ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),