# HG changeset patch
# User wenzelm
# Date 1136496597 -3600
# Node ID 588e802896589bcaf40258023c3b5be4682ec57b
# Parent  5d379fe2eb741755f93ae0520f293e3683c0fdc1
store_thm: transfer to current context, i.e. the target theory;

diff -r 5d379fe2eb74 -r 588e80289658 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Jan 05 22:29:55 2006 +0100
+++ b/src/Provers/classical.ML	Thu Jan 05 22:29:57 2006 +0100
@@ -229,7 +229,7 @@
 (*** Useful tactics for classical reasoning ***)
 
 val imp_elim = (*cannot use bind_thm within a structure!*)
-  store_thm ("imp_elim", classical_rule (Tactic.make_elim mp));
+  store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
 
 (*Prove goal that assumes both P and ~P.
   No backtracking if it finds an equal assumption.  Perhaps should call
@@ -245,7 +245,8 @@
 fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
 
 val swap =
-  store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
+  store_thm ("swap", Thm.transfer (the_context ())
+    (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
 
 (*Creates rules to eliminate ~A, from rules to introduce A*)
 fun swapify intrs = intrs RLN (2, [swap]);