# HG changeset patch
# User chaieb
# Date 1127216007 -7200
# Node ID b053d5a89b6f7b3bafab7800c284b2ecb9bc1a11
# Parent  8836793df94741e335e35dfb62f37a589af4de30
The simpset of the actual theory is take, in order to handle rings defined after the method

diff -r 8836793df947 -r b053d5a89b6f src/HOL/Tools/comm_ring.ML
--- a/src/HOL/Tools/comm_ring.ML	Tue Sep 20 13:17:55 2005 +0200
+++ b/src/HOL/Tools/comm_ring.ML	Tue Sep 20 13:33:27 2005 +0200
@@ -107,7 +107,7 @@
 (*The cring tactic  *)
 (* Attention: You have to make sure that no t^0 is in the goal!! *)
 (* Use simply rewriting t^0 = 1 *)
-val cring_ss = simpset_of (the_context())
+fun cring_ss sg = simpset_of sg
                            addsimps
                            (map thm ["mkPX_def", "mkPinj_def","sub_def",
                                      "power_add","even_def","pow_if"])
@@ -119,12 +119,12 @@
         val g = List.nth (prems_of st, i - 1)
         val sg = sign_of_thm st
         val (ca,cvs,clhs,crhs) = reif_eq sg (HOLogic.dest_Trueprop g)
-        val norm_eq_th = simplify cring_ss
+        val norm_eq_th = simplify (cring_ss sg)
                         (instantiate' [SOME ca] [SOME clhs, SOME crhs, SOME cvs]
                                                 norm_eq)
     in ((cut_rules_tac [norm_eq_th] i)
-            THEN (simp_tac cring_ss i)
-            THEN (simp_tac cring_ss i)) st
+            THEN (simp_tac (cring_ss sg) i)
+            THEN (simp_tac (cring_ss sg) i)) st
     end);
 
 fun comm_ring_method i = Method.METHOD (fn facts =>