diff -r 6ce832f71bdd -r ff1ec795604b src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Mon May 20 18:38:28 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Mon May 20 20:47:33 2013 +0200
@@ -3487,7 +3487,7 @@
                                      (@{cpat "?prec::nat"}, p),
                                      (@{cpat "?ss::nat list"}, s)])
               @{thm "approx_form"}) i
-          THEN simp_tac @{context} i) st
+          THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st
        end
 
      | SOME t => if length vs <> 1 then raise (TERM ("More than one variable used for taylor series expansion", [prop_of st]))
@@ -3531,7 +3531,7 @@
       REPEAT (FIRST' [etac @{thm intervalE},
                       etac @{thm meta_eqE},
                       rtac @{thm impI}] i)
-      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) @{context} i
+      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i
       THEN DETERM (TRY (filter_prems_tac (K false) i))
       THEN DETERM (Reflection.gen_reify_tac ctxt form_equations NONE i)
       THEN rewrite_interpret_form_tac ctxt prec splitting taylor i
@@ -3621,33 +3621,33 @@
        |> HOLogic.dest_Trueprop
        |> HOLogic.dest_eq |> snd
 
-  fun apply_tactic context term tactic = cterm_of context term
+  fun apply_tactic ctxt term tactic =
+    cterm_of (Proof_Context.theory_of ctxt) term
     |> Goal.init
     |> SINGLE tactic
     |> the |> prems_of |> hd
 
-  fun prepare_form context term = apply_tactic context term (
+  fun prepare_form ctxt term = apply_tactic ctxt term (
       REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1)
-      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) @{context} 1
+      THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1
       THEN DETERM (TRY (filter_prems_tac (K false) 1)))
 
-  fun reify_form context term = apply_tactic context term
-     (Reflection.gen_reify_tac @{context} form_equations NONE 1)
+  fun reify_form ctxt term = apply_tactic ctxt term
+     (Reflection.gen_reify_tac ctxt form_equations NONE 1)
 
   fun approx_form prec ctxt t =
           realify t
-       |> prepare_form (Proof_Context.theory_of ctxt)
-       |> (fn 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"}
-            (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
-       |> approximate ctxt
-       |> HOLogic.dest_list
-       |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
-       |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
-       |> foldr1 HOLogic.mk_conj))
+       |> prepare_form ctxt
+       |> (fn arith_term => reify_form 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"}
+                (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs)))
+           |> approximate ctxt
+           |> HOLogic.dest_list
+           |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
+           |> map (fn (elem, s) => @{term "op : :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
+           |> foldr1 HOLogic.mk_conj))
 
   fun approx_arith prec ctxt t = realify t
        |> Reflection.gen_reify ctxt form_equations