# HG changeset patch
# User wenzelm
# Date 959776032 -7200
# Node ID 963b7eb1b57b7829b3f4571c6593a03282ce8ae5
# Parent  135c998d2b468f930c0b4c19dafa2f836b9a95ad
removed 'transfer' att (is now automatic);

diff -r 135c998d2b46 -r 963b7eb1b57b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed May 31 14:26:46 2000 +0200
+++ b/src/Pure/Isar/attrib.ML	Wed May 31 14:27:12 2000 +0200
@@ -175,14 +175,6 @@
 fun gen_untag x = syntax (Scan.lift Args.name >> Drule.untag) x;
 
 
-(* transfer *)
-
-fun gen_transfer theory_of = no_args (Drule.rule_attribute (fn st => Thm.transfer (theory_of st)));
-
-val global_transfer = gen_transfer I;
-val local_transfer = gen_transfer ProofContext.theory_of;
-
-
 (* COMP *)
 
 fun comp (i, B) (x, A) = (x, Drule.compose_single (A, i, B));
@@ -308,7 +300,6 @@
   ("elimify", (elimify, elimify), "turn destruct rule into elimination rule"),
   ("case_names", (case_names, case_names), "name rule cases"),
   ("params", (params, params), "name rule parameters"),
-  ("transfer", (global_transfer, local_transfer), "transfer theorem to this theory"),
   ("export", (global_export, local_export), "export theorem from context")];