diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index cef2681da0c81e999a7294f1f4aaaed16c968c0f..a2a97564c5ebfd7d8724720ce1500f9d13c865f6 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -122,8 +122,12 @@ let converter d (f : Ground.t) =
    app = { builtin = Expr.Destructor { case; field; adt; _ }; _ };
    args;
    tyargs;
+   ty;
    _;
   } ->
+      (* not completely satisfactory but needed, it is not yet clear who has the responsibility of choice for booleans *)
+      if Ground.Ty.(equal ty bool) then
+        Choice.register_thterm d (Ground.thterm f) (Boolean.chobool r);
       let case = case_of_int case in
       let field = field_of_int field in
       let adt = Option.value_exn (Adt_value.MonoAdt.index adt tyargs) in