The simpset of the actual theory is take, in order to handle rings defined after the method
authorchaieb
Tue Sep 20 13:33:27 2005 +0200 (2005-09-20)
changeset 17503b053d5a89b6f
parent 17502 8836793df947
child 17504 cc10c4b64b8e
The simpset of the actual theory is take, in order to handle rings defined after the method
src/HOL/Tools/comm_ring.ML
     1.1 --- a/src/HOL/Tools/comm_ring.ML	Tue Sep 20 13:17:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/comm_ring.ML	Tue Sep 20 13:33:27 2005 +0200
     1.3 @@ -107,7 +107,7 @@
     1.4  (*The cring tactic  *)
     1.5  (* Attention: You have to make sure that no t^0 is in the goal!! *)
     1.6  (* Use simply rewriting t^0 = 1 *)
     1.7 -val cring_ss = simpset_of (the_context())
     1.8 +fun cring_ss sg = simpset_of sg
     1.9                             addsimps
    1.10                             (map thm ["mkPX_def", "mkPinj_def","sub_def",
    1.11                                       "power_add","even_def","pow_if"])
    1.12 @@ -119,12 +119,12 @@
    1.13          val g = List.nth (prems_of st, i - 1)
    1.14          val sg = sign_of_thm st
    1.15          val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
    1.16 -        val norm_eq_th = simplify cring_ss
    1.17 +        val norm_eq_th = simplify (cring_ss sg)
    1.18                          (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
    1.19                                                  norm_eq)
    1.20      in ((cut_rules_tac [norm_eq_th] i)
    1.21 -            THEN (simp_tac cring_ss i)
    1.22 -            THEN (simp_tac cring_ss i)) st
    1.23 +            THEN (simp_tac (cring_ss sg) i)
    1.24 +            THEN (simp_tac (cring_ss sg) i)) st
    1.25      end);
    1.26  
    1.27  fun comm_ring_method i = Method.METHOD (fn facts =>