diff -r 867ca0d92ea2 -r f17a1c60ac39 src/HOL/Decision_Procs/approximation_generator.ML
--- a/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 21 17:56:25 2016 +0200
+++ b/src/HOL/Decision_Procs/approximation_generator.ML	Wed Sep 21 17:56:25 2016 +0200
@@ -55,6 +55,7 @@
   | mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs)
   | mapprox_floatarith (@{term Power} $ a $ n) xs =
       Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n))
+  | mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs))
   | mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n)
   | mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m
   | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t])
@@ -130,7 +131,13 @@
           (map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $
         @{term "[] :: nat list"}
   in
-    (if mapprox_form eps e (map (real_of_Float o fst) rs)
+    (if
+      mapprox_form eps e (map (real_of_Float o fst) rs)
+      handle
+        General.Overflow => false
+      | General.Domain => false
+      | General.Div => false
+      | IEEEReal.Unordered => false
     then
       let
         val ts = map (fn x => snd x ()) rs