diff --git a/src/language.ml b/src/language.ml
index 39afa6c1b39a9ca36d8dabf0a0db9ffee5cbafa3..05ad16db554996d592a0978cbb52b4ea4ff9bf78 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -160,14 +160,14 @@ let register_ovo_support () =
 
 let vectors = Term.Hls.create 10
 
-let vector_elt_ty env =
+let float64_t_ty env =
   let th = Env.read_theory env [ "ieee_float" ] "Float64" in
   Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
 
 let create_vector =
   Env.Wenv.memoize 13 (fun env ->
     let h = Hashtbl.create (module Int) in
-    let ty_elt = vector_elt_ty env in
+    let ty_elt = float64_t_ty env in
     let ty =
       let th = Env.read_theory env [ "interpretation" ] "Vector" in
       Ty.ty_app (Theory.ns_find_ts th.th_export [ "vector" ]) [ ty_elt ]
@@ -207,10 +207,7 @@ let fresh_nn_ls env name =
 let create_nn_nnet =
   Env.Wenv.memoize 13 (fun env ->
     let h = Hashtbl.create (module String) in
-    let ty_elt =
-      let th = Env.read_theory env [ "ieee_float" ] "Float64" in
-      Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
-    in
+    let ty_elt = float64_t_ty env in
     Hashtbl.findi_or_add h ~default:(fun filename ->
       let ls = fresh_nn_ls env "nnet_nn" in
       let nn =
@@ -232,7 +229,7 @@ let create_nn_nnet =
 let create_nn_onnx =
   Env.Wenv.memoize 13 (fun env ->
     let h = Hashtbl.create (module String) in
-    let ty_elt = vector_elt_ty env in
+    let ty_elt = float64_t_ty env in
     Hashtbl.findi_or_add h ~default:(fun filename ->
       let ls = fresh_nn_ls env "onnx_nn" in
       let onnx =