--- a/src/HOL/Decision_Procs/approximation_generator.ML Mon Nov 04 19:53:43 2019 -0500
+++ b/src/HOL/Decision_Procs/approximation_generator.ML Sun Nov 03 21:46:46 2019 -0500
@@ -92,6 +92,10 @@
fun real_of_Float (@{code Float} (m, e)) =
real_of_man_exp (@{code integer_of_int} m) (@{code integer_of_int} e)
+fun term_of_int i = (HOLogic.mk_number @{typ int} (@{code integer_of_int} i))
+
+fun term_of_Float (@{code Float} (m, e)) = @{term Float} $ term_of_int m $ term_of_int e
+
fun is_True \<^term>\<open>True\<close> = true
| is_True _ = false
@@ -142,7 +146,7 @@
| IEEEReal.Unordered => false
then
let
- val ts = map (fn x => snd x ()) rs
+ val ts = map (fn x => term_of_Float (fst x)) rs
val ts' = map
(AList.lookup op = (map dest_Free xs ~~ ts)
#> the_default Term.dummy