src/HOL/Decision_Procs/mir_tac.ML

--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 16:15:37 2011 +0200
@@ -94,7 +94,7 @@
         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_mir thy q g
     (* Some simpsets for dealing with mod div abs and nat*)