src/HOL/Decision_Procs/cooper_tac.ML

--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -69,7 +69,7 @@
 fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
-    val thy = ProofContext.theory_of ctxt
+    val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
     val (t,np,nh) = prepare_for_linz q g
     (* Some simpsets for dealing with mod div abs and nat*)