
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 \<Rightarrow> real set \<Rightarrow> 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




