diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml
index e88b94967..1ba519ec4 100644
--- a/src/lib/frontend/d_cnf.ml
+++ b/src/lib/frontend/d_cnf.ml
@@ -1081,18 +1081,19 @@ let rec mk_expr
 
           | B.Destructor { case; field; adt; _ }, [x] ->
             begin match DT.definition adt with
-              | Some (Adt { cases; record; _ }) ->
+              | Some (Adt { cases;  _ }) ->
                 begin match cases.(case).dstrs.(field) with
                   | Some { path; _ } ->
                     let name = get_basename path in
                     let ty = dty_to_ty term_ty in
                     let e = aux_mk_expr x in
                     let sy =
-                      if record || Array.length cases = 1
-                      then
+                      match Cache.find_ty (DE.Ty.Const.hash adt) with
+                      | Trecord _ ->
                         Sy.Op (Sy.Access (Hstring.make name))
-                      else
+                      | Tadt _ ->
                         Sy.destruct ~guarded:true name
+                      | _ -> assert false
                     in
                     E.mk_term sy [e] ty
                   | _ ->
diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli
index 895bac4e2..5d0199daf 100644
--- a/src/lib/structures/ty.mli
+++ b/src/lib/structures/ty.mli
@@ -175,7 +175,7 @@ val t_adt :
   ?body: ((string * (string * t) list) list) option ->
   string -> t list ->
   t
-(** Crearte and algebraic datatype. The body is a list of
+(** Create an algebraic datatype. The body is a list of
     constructors, where each constructor is associated with the list of
     its destructors with their respective types. If [body] is none,
     then no definition will be registered for this type. The second