diff --git a/src/smt/Solver_types.ml b/src/smt/Solver_types.ml
index f88b317f..de1ea2fe 100644
--- a/src/smt/Solver_types.ml
+++ b/src/smt/Solver_types.ml
@@ -42,7 +42,6 @@ and cst_view =
       do_cc: bool; (* participate in congruence closure? *)
       relevant : 'a. ID.t -> 'a IArray.t -> int -> bool; (* relevant argument? *)
       ty : ID.t -> term IArray.t -> ty; (* compute type *)
-      is_value: bool; (* value constructor *)
       eval: value IArray.t -> value; (* evaluate term *)
     }
 (** Methods on the custom term view whose arguments are ['a].
diff --git a/src/smt/Term.ml b/src/smt/Term.ml
index d0223da2..b61b608b 100644
--- a/src/smt/Term.ml
+++ b/src/smt/Term.ml
@@ -61,9 +61,6 @@ let create ?(size=1024) () : state =
   ignore (Lazy.force st.false_); (* not true *)
   st
 
-let[@inline] all_terms st = Term_cell.Tbl.values st.tbl
-let[@inline] is_value t = Term_cell.is_value t.term_view
-
 let app_cst st f a =
   let cell = Term_cell.app_cst f a in
   make st cell
diff --git a/src/smt/Term.mli b/src/smt/Term.mli
index 5e47042b..2a7da645 100644
--- a/src/smt/Term.mli
+++ b/src/smt/Term.mli
@@ -39,13 +39,8 @@ val abs : t -> t * bool
 
 val to_seq : t -> t Sequence.t
 
-val all_terms : state -> t Sequence.t
-
 val pp : t Fmt.printer
 
-val is_value : t -> bool
-(** Values are special terms that behave specially wrt congruence/equality *)
-
 (** {6 Views} *)
 
 val is_true : t -> bool
diff --git a/src/smt/Term_cell.ml b/src/smt/Term_cell.ml
index b873e3c5..6f9e248d 100644
--- a/src/smt/Term_cell.ml
+++ b/src/smt/Term_cell.ml
@@ -53,11 +53,6 @@ include Make_eq(struct
 let true_ = Bool true
 let false_ = Bool false
 
-let is_value = function
-  | Bool _ -> true
-  | App_cst ({cst_view=Cst_def r;_}, _) -> r.is_value
-  | If _ | App_cst _ | Eq _ -> false
-
 let app_cst f a = App_cst (f, a)
 let const c = App_cst (c, IArray.empty)
 let eq a b =
diff --git a/src/smt/Term_cell.mli b/src/smt/Term_cell.mli
index cce393b4..a7689c99 100644
--- a/src/smt/Term_cell.mli
+++ b/src/smt/Term_cell.mli
@@ -19,8 +19,6 @@ val app_cst : cst -> term IArray.t -> t
 val eq : term -> term -> t
 val if_ : term -> term -> term -> t
 
-val is_value : t -> bool
-
 val ty : t -> Ty.t
 (** Compute the type of this term cell. Not totally free *)
 
diff --git a/src/th-bool/Bool_term.ml b/src/th-bool/Bool_term.ml
index be17cfd0..6a405911 100644
--- a/src/th-bool/Bool_term.ml
+++ b/src/th-bool/Bool_term.ml
@@ -86,7 +86,7 @@ module C = struct
   let mk_cst ?(do_cc=false) id : cst =
     {cst_id=id;
      cst_view=Cst_def {
-         pp=None; abs; ty=get_ty; relevant; is_value=false; do_cc; eval=eval id; }; }
+         pp=None; abs; ty=get_ty; relevant; do_cc; eval=eval id; }; }
 
   let not = mk_cst id_not
   let and_ = mk_cst id_and