--- a/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:09 2009 +0200
@@ -89,7 +89,7 @@
fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
let
val thy = ProofContext.theory_of ctxt;
- val cring_ss = Simplifier.local_simpset_of ctxt (*FIXME really the full simpset!?*)
+ val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*)
addsimps cring_simps;
val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
val norm_eq_th =