diff -r 37adfa07b54b -r ccfb774af58c src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue Oct 13 12:02:55 2009 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Tue Oct 13 13:40:26 2009 +0200 @@ -3473,7 +3473,7 @@ |> HOLogic.dest_list |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term) |> map (fn (elem, s) => @{term "op : :: real \ real set \ bool"} $ elem $ mk_result prec (dest_ivl s)) - |> foldl1 HOLogic.mk_conj)) + |> foldr1 HOLogic.mk_conj)) fun approx_arith prec ctxt t = realify t |> Reflection.genreif ctxt form_equations