--- a/src/HOL/Decision_Procs/approximation_generator.ML Sun Nov 03 19:58:02 2019 -0500
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Sun Nov 03 19:59:56 2019 -0500
@@ -133,8 +133,8 @@
\<^const>\<open>approx_form\<close> $
HOLogic.mk_number \<^typ>\<open>nat\<close> prec $
e $
- (HOLogic.mk_list \<^typ>\<open>(float * float) option\<close>
- (map (fn t => mk_Some \<^typ>\<open>float * float\<close> $ HOLogic.mk_prod (t, t)) ts)) $
+ (HOLogic.mk_list \<^typ>\<open>(float interval) option\<close>
+ (map (fn t => mk_Some \<^typ>\<open>float interval\<close> $ (\<^term>\<open>interval_of::float\<Rightarrow>_\<close> $ t)) ts)) $
\<^term>\<open>[] :: nat list\<close>
in
(if