diff -r da8817d01e7c -r 23f352990944 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 16 15:47:52 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 16 16:15:37 2011 +0200
@@ -3341,10 +3341,10 @@
     end
 
   fun approximation_conv ctxt ct =
-    approximation_oracle (ProofContext.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
+    approximation_oracle (Proof_Context.theory_of ctxt, Thm.term_of ct |> tap (tracing o Syntax.string_of_term ctxt));
 
   fun approximate ctxt t =
-    approximation_oracle (ProofContext.theory_of ctxt, t)
+    approximation_oracle (Proof_Context.theory_of ctxt, t)
     |> Thm.prop_of |> Logic.dest_equals |> snd;
 
   (* Should be in HOL.thy ? *)
@@ -3366,16 +3366,16 @@
                |> HOLogic.dest_list
       val p = prec
               |> HOLogic.mk_number @{typ nat}
-              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
     in case taylor
     of NONE => let
          val n = vs |> length
                  |> HOLogic.mk_number @{typ nat}
-                 |> Thm.cterm_of (ProofContext.theory_of ctxt)
+                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
          val s = vs
                  |> map lookup_splitting
                  |> HOLogic.mk_list @{typ nat}
-                 |> Thm.cterm_of (ProofContext.theory_of ctxt)
+                 |> Thm.cterm_of (Proof_Context.theory_of ctxt)
        in
          (rtac (Thm.instantiate ([], [(@{cpat "?n::nat"}, n),
                                      (@{cpat "?prec::nat"}, p),
@@ -3388,9 +3388,9 @@
        else let
          val t = t
               |> HOLogic.mk_number @{typ nat}
-              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
          val s = vs |> map lookup_splitting |> hd
-              |> Thm.cterm_of (ProofContext.theory_of ctxt)
+              |> Thm.cterm_of (Proof_Context.theory_of ctxt)
        in
          rtac (Thm.instantiate ([], [(@{cpat "?s::nat"}, s),
                                      (@{cpat "?t::nat"}, t),
@@ -3530,9 +3530,9 @@
 
   fun approx_form prec ctxt t =
           realify t
-       |> prepare_form (ProofContext.theory_of ctxt)
+       |> prepare_form (Proof_Context.theory_of ctxt)
        |> (fn arith_term =>
-          reify_form (ProofContext.theory_of ctxt) arith_term
+          reify_form (Proof_Context.theory_of ctxt) arith_term
        |> HOLogic.dest_Trueprop |> dest_interpret_form
        |> (fn (data, xs) =>
           mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"}