store_thm: transfer to current context, i.e. the target theory;
authorwenzelm
Thu Jan 05 22:29:57 2006 +0100 (2006-01-05 ago)
changeset 18586588e80289658
parent 18585 5d379fe2eb74
child 18587 d4dcdfd764a0
store_thm: transfer to current context, i.e. the target theory;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Thu Jan 05 22:29:55 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Jan 05 22:29:57 2006 +0100
     1.3 @@ -229,7 +229,7 @@
     1.4  (*** Useful tactics for classical reasoning ***)
     1.5  
     1.6  val imp_elim = (*cannot use bind_thm within a structure!*)
     1.7 -  store_thm ("imp_elim", classical_rule (Tactic.make_elim mp));
     1.8 +  store_thm ("imp_elim", Thm.transfer (the_context ()) (classical_rule (Tactic.make_elim mp)));
     1.9  
    1.10  (*Prove goal that assumes both P and ~P.
    1.11    No backtracking if it finds an equal assumption.  Perhaps should call
    1.12 @@ -245,7 +245,8 @@
    1.13  fun eq_mp_tac i = ematch_tac [not_elim, imp_elim] i  THEN  eq_assume_tac i;
    1.14  
    1.15  val swap =
    1.16 -  store_thm ("swap", rule_by_tactic (etac thin_rl 1) (not_elim RS classical));
    1.17 +  store_thm ("swap", Thm.transfer (the_context ())
    1.18 +    (rule_by_tactic (etac thin_rl 1) (not_elim RS classical)));
    1.19  
    1.20  (*Creates rules to eliminate ~A, from rules to introduce A*)
    1.21  fun swapify intrs = intrs RLN (2, [swap]);