author chaieb Tue, 20 Sep 2005 13:33:27 +0200 changeset 17503 b053d5a89b6f parent 17502 8836793df947 child 17504 cc10c4b64b8e
The simpset of the actual theory is take, in order to handle rings defined after the method
```--- 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
(map thm ["mkPX_def", "mkPinj_def","sub_def",
@@ -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 =>```