diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml
index fdc2373c0..12c74f1cd 100644
--- a/src/lib/frontend/typechecker.ml
+++ b/src/lib/frontend/typechecker.ml
@@ -272,8 +272,7 @@ module Env = struct
     let ty = Fpa_rounding.fpa_rounding_mode in
     match ty with
     | Ty.Tadt (name, []) ->
-      let Ty.{ cases; kind } = Ty.type_body name [] in
-      assert (Stdlib.(kind = Ty.Enum));
+      let cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.fold_left
         (fun m c ->
@@ -299,8 +298,7 @@ module Env = struct
   let find_builtin_cstr ty n =
     match ty with
     | Ty.Tadt (name, []) ->
-      let Ty.{ cases; kind } = Ty.type_body name [] in
-      assert (Stdlib.(kind = Ty.Enum));
+      let cases = Ty.type_body name [] in
       let cstrs = List.map (fun Ty.{ constr; _ } -> constr) cases in
       List.find (Uid.equal n) cstrs
     | _ ->
@@ -1003,9 +1001,7 @@ let rec type_term ?(call_from_type_form=false) env f =
       let e = type_term env e in
       let ty = Ty.shorten e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
-          let Ty.{ cases; _ } = Ty.type_body name params in
-          cases
+        | Ty.Tadt (name, params) -> Ty.type_body name params
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr; destrs = lbs}]
         | _ -> Errors.typing_error (ShouldBeADT ty) loc
@@ -1411,9 +1407,7 @@ and type_form ?(in_theory=false) env f =
       let e = type_term env e in
       let ty = e.c.tt_ty in
       let ty_body = match ty with
-        | Ty.Tadt (name, params) ->
-          let Ty.{ cases; _ } = Ty.type_body name params in
-          cases
+        | Ty.Tadt (name, params) -> Ty.type_body name params
         | Ty.Trecord { Ty.record_constr; lbs; _ } ->
           [{Ty.constr = record_constr ; destrs = lbs}]
 
diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml
index be34ff793..feb25c96a 100644
--- a/src/lib/reasoners/adt.ml
+++ b/src/lib/reasoners/adt.ml
@@ -56,7 +56,7 @@ let constr_of_destr ty dest =
   match ty with
   | Ty.Tadt (s, params) ->
     begin
-      let Ty.{ cases; _ } = Ty.type_body s params in
+      let cases = Ty.type_body s params in
       try
         List.find
           (fun { Ty.destrs; _ } ->
@@ -174,7 +174,7 @@ module Shostak (X : ALIEN) = struct
     let xs = List.rev sx in
     match f, xs, ty with
     | Sy.Op Sy.Constr hs, _, Ty.Tadt (name, params) ->
-      let Ty.{ cases; _ } = Ty.type_body name params in
+      let cases = Ty.type_body name params in
       let case_hs =
         try Ty.assoc_destrs hs cases with Not_found -> assert false
       in
diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml
index 612a31cac..18eb871b3 100644
--- a/src/lib/reasoners/adt_rel.ml
+++ b/src/lib/reasoners/adt_rel.ml
@@ -85,7 +85,7 @@ module Domain = struct
     match ty with
     | Ty.Tadt (name, params) ->
       (* Return the list of all the constructors of the type of [r]. *)
-      let Ty.{ cases; _ } = Ty.type_body name params in
+      let cases = Ty.type_body name params in
       let constrs =
         List.fold_left
           (fun acc Ty.{ constr; _ } ->
@@ -116,6 +116,8 @@ module Domain = struct
     let constrs = TSet.remove c d.constrs in
     let ex = Ex.union ex d.ex in
     domain ~constrs ex
+
+  let for_all f { constrs; _ } = TSet.for_all f constrs
 end
 
 let is_adt_ty = function
@@ -134,7 +136,10 @@ module Domains = struct
         We don't store domains for constructors and selectors. *)
 
     enums: SX.t;
-    (** Set of tracked representatives of enum type. *)
+    (** Set of tracked representatives whose the domain only contains
+        enum constructors, that is constructors without payload.
+
+        This field is used by the case split mechanism, see [pick_enum]. *)
 
     changed : SX.t;
     (** Representatives whose domain has changed since the last flush
@@ -154,19 +159,24 @@ module Domains = struct
 
   let filter_ty = is_adt_ty
 
-  let is_enum r =
+  (* TODO: This test is slow because we have to retrieve the list of
+     destructors of the constructor [c] by searching in the list [cases].
+
+     A better predicate will be easy to implement after getting rid of
+     the legacy frontend and switching from [Uid.t] to
+     [Dolmen.Std.Expr.term_cst] to store the constructors. Indeed, [term_cst]
+     contains the type of constructor and in particular its arity. *)
+  let is_enum_cstr r c =
     match X.type_info r with
-    | Ty.Tadt (name, params) ->
-      let Ty.{ kind; _ } = Ty.type_body name params in
-      begin match kind with
-        | Enum -> true
-        | Adt -> false
-      end
-    | _ -> false
+    | Tadt (name, args) ->
+      let cases = Ty.type_body name args in
+      Lists.is_empty @@ Ty.assoc_destrs c cases
+    | _ -> assert false
 
   let internal_update r nd t =
     let domains = MX.add r nd t.domains in
-    let enums = if is_enum r then SX.add r t.enums else t.enums in
+    let is_enum_domain = Domain.for_all (is_enum_cstr r) nd in
+    let enums = if is_enum_domain then SX.add r t.enums else t.enums in
     let changed = SX.add r t.changed in
     { domains; enums; changed }
 
@@ -483,7 +493,7 @@ let build_constr_eq r c =
   | Alien r ->
     begin match X.type_info r with
       | Ty.Tadt (name, params) as ty ->
-        let Ty.{ cases; _ } = Ty.type_body name params in
+        let cases = Ty.type_body name params in
         let ds =
           try Ty.assoc_destrs c cases with Not_found -> assert false
         in
@@ -585,7 +595,7 @@ let constr_of_destr ty d =
   match ty with
   | Ty.Tadt (name, params) ->
     begin
-      let Ty.{ cases; _ } = Ty.type_body name params in
+      let cases = Ty.type_body name params in
       try
         let r =
           List.find
diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml
index 0f2dcafbf..a3d3f2268 100644
--- a/src/lib/structures/ty.ml
+++ b/src/lib/structures/ty.ml
@@ -72,13 +72,7 @@ type adt_constr =
   { constr : Uid.t ;
     destrs : (Uid.t * t) list }
 
-type adt_kind = Enum | Adt
-
-type type_body = {
-  cases : adt_constr list;
-  kind : adt_kind
-}
-
+type type_body = adt_constr list
 
 let assoc_destrs hs cases =
   let res = ref None in
@@ -145,7 +139,7 @@ let print_generic body_of =
         begin match body_of with
           | None -> ()
           | Some type_body ->
-            let { cases; _ } = type_body n lv in
+            let cases = type_body n lv in
             fprintf fmt " = {";
             let first = ref true in
             List.iter
@@ -434,9 +428,8 @@ module Decls = struct
   let (decls : decls ref) = ref MH.empty
 
 
-  let fresh_type params body =
+  let fresh_type params cases =
     let params, subst = fresh_list params esubst in
-    let { cases; kind } = body in
     let _subst, cases =
       List.fold_left
         (fun (subst, cases) {constr; destrs} ->
@@ -450,7 +443,7 @@ module Decls = struct
            subst, {constr; destrs} :: cases
         )(subst, []) (List.rev cases)
     in
-    params, { cases; kind }
+    params, cases
 
 
   let add name params body =
@@ -471,7 +464,7 @@ module Decls = struct
         else MTY.find args instances
       (* should I instantiate if not found ?? *)
       with Not_found ->
-        let params, body = fresh_type params body in
+        let params, cases = fresh_type params body in
         (*if true || get_debug_adt () then*)
         let sbt =
           try
@@ -489,21 +482,17 @@ module Decls = struct
               )M.empty params args
           with Invalid_argument _ -> assert false
         in
-        let body =
-          let { cases; kind } = body in
-          let cases =
-            List.map
-              (fun {constr; destrs} ->
-                 {constr;
-                  destrs =
-                    List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs }
-              ) cases
-          in
-          { cases; kind }
+        let cases =
+          List.map
+            (fun {constr; destrs} ->
+               {constr;
+                destrs =
+                  List.map (fun (d, ty) -> d, apply_subst sbt ty) destrs }
+            ) cases
         in
         let params = List.map (fun ty -> apply_subst sbt ty) params in
-        add name params body;
-        body
+        add name params cases;
+        cases
     with Not_found ->
       Printer.print_err "%a not found" Uid.pp name;
       assert false
@@ -543,20 +532,12 @@ let t_adt ?(body=None) s ty_vars =
       let cases =
         List.map (fun (constr, destrs) -> {constr; destrs}) cases
       in
-      let is_enum =
-        List.for_all (fun { destrs; _ } -> Lists.is_empty destrs) cases
-      in
-      let kind = if is_enum then Enum else Adt in
-      Decls.add s ty_vars { cases; kind }
+      Decls.add s ty_vars cases
     | Some cases ->
       let cases =
         List.map (fun (constr, destrs) -> {constr; destrs}) cases
       in
-      let is_enum =
-        List.for_all (fun { destrs; _ } -> Lists.is_empty destrs) cases
-      in
-      let kind = if is_enum then Enum else Adt in
-      Decls.add s ty_vars { cases; kind }
+      Decls.add s ty_vars cases
   end;
   ty
 
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 2b730c67a..2b3a38eb5 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -99,21 +99,10 @@ type adt_constr =
         their respective types *)
   }
 
-type adt_kind =
-  | Enum (* ADT whose all the constructors have no payload. *)
-  | Adt
-
 (** Bodies of types definitions. Currently, bodies are inlined in the
     type [t] for records and enumerations. But, this is not possible
     for recursive ADTs *)
-type type_body = {
-  cases : adt_constr list;
-  (** body of an algebraic datatype *)
-
-  kind : adt_kind
-  (** This flag is used by the case splitting mechanism of the ADT theory.
-      We perform eager splitting on ADT of kind [enum]. *)
-}
+type type_body = adt_constr list
 
 module Svty : Set.S with type elt = int
 (** Sets of type variables, indexed by their identifier. *)