src/HOL/Decision_Procs/Approximation.thy

--- a/src/HOL/Decision_Procs/Approximation.thy	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Fri May 31 09:30:32 2013 +0200
@@ -3650,10 +3650,10 @@
            |> foldr1 HOLogic.mk_conj))
 
   fun approx_arith prec ctxt t = realify t
+       |> Thm.cterm_of (Proof_Context.theory_of ctxt)
        |> Reflection.reify ctxt form_equations
        |> prop_of
-       |> HOLogic.dest_Trueprop
-       |> HOLogic.dest_eq |> snd
+       |> Logic.dest_equals |> snd
        |> dest_interpret |> fst
        |> mk_approx' prec
        |> approximate ctxt