diff --git a/src/interpretation.ml b/src/interpretation.ml
index 605e68de649d01d92abb0d2ef3d3753c20361f34..15f367d3ff29230325a9d41a5539af49a5d292f6 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -25,13 +25,13 @@ open Why3
 open Base
 
 type classifier =
-  | NNet of Language.nn_classifier
+  | NNet of Term.lsymbol
       [@printer
         fun fmt nn ->
           Fmt.pf fmt "NNet: %a"
             Fmt.(option Language.pp_nn)
             (Language.lookup_nn_classifier nn)]
-  | ONNX of Language.nn_classifier
+  | ONNX of Term.lsymbol
       [@printer
         fun fmt nn ->
           Fmt.pf fmt "ONNX: %a"
@@ -45,7 +45,7 @@ type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
 type data = D_csv of string list [@@deriving show]
 
 type vector =
-  (Language.vector
+  (Term.lsymbol
   [@printer
     fun fmt v ->
       Fmt.pf fmt "%a" Fmt.(option ~none:nop int) (Language.lookup_vector v)])
diff --git a/src/language.ml b/src/language.ml
index 75a9dac26f86968e684a884ed442a51fa9bc29a9..3c7db414e837f38dfb5e357c4e8c6baef98ae42a 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -158,8 +158,6 @@ let register_ovo_support () =
 
 (* -- Vector *)
 
-type vector = Term.lsymbol
-
 let vectors = Term.Hls.create 10
 
 let vector_elt_ty env =
@@ -196,8 +194,6 @@ type nn = {
 }
 [@@deriving show]
 
-type nn_classifier = Term.lsymbol
-
 let nn_classifiers = Term.Hls.create 10
 
 let fresh_classifier_ls env name =
diff --git a/src/language.mli b/src/language.mli
index 52ed49a99deb73952d7439f970afb62ad7a91320..4ac58bcf338eb7d45106590697eed67a3332b33c 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -65,11 +65,9 @@ val ovo_parser : Env.env -> string -> Pmodule.pmodule Wstdlib.Mstr.t
 
 (** -- Vector *)
 
-type vector = Term.lsymbol
-
-val create_vector : Env.env -> int -> vector
-val lookup_vector : vector -> int option
-val mem_vector : vector -> bool
+val create_vector : Env.env -> int -> Term.lsymbol
+val lookup_vector : Term.lsymbol -> int option
+val mem_vector : Term.lsymbol -> bool
 
 (** -- Classifier *)
 
@@ -82,9 +80,7 @@ type nn = private {
 }
 [@@deriving show]
 
-type nn_classifier = Term.lsymbol
-
-val create_nnet_classifier : Env.env -> string -> nn_classifier
-val create_onnx_classifier : Env.env -> string -> nn_classifier
-val lookup_nn_classifier : nn_classifier -> nn option
-val mem_nn_classifier : nn_classifier -> bool
+val create_nnet_classifier : Env.env -> string -> Term.lsymbol
+val create_onnx_classifier : Env.env -> string -> Term.lsymbol
+val lookup_nn_classifier : Term.lsymbol -> nn option
+val mem_nn_classifier : Term.lsymbol -> bool