src/HOL/Decision_Procs/commutative_ring_tac.ML

--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -86,7 +86,7 @@
 
 fun tac ctxt = SUBGOAL (fn (g, i) =>
   let
-    val thy = ProofContext.theory_of ctxt;
+    val thy = Proof_Context.theory_of ctxt;
     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)