diff --git a/src/core/Sidekick_core.ml b/src/core/Sidekick_core.ml
index b2f9b6c5..82d56a19 100644
--- a/src/core/Sidekick_core.ml
+++ b/src/core/Sidekick_core.ml
@@ -626,17 +626,6 @@ module type SOLVER = sig
     val sign : t -> bool
   end
 
-  (* FIXME: just use terms instead? *)
-  (** {3 Semantic values} *)
-  module Value : sig
-    type t
-
-    val equal : t -> t -> bool
-    val hash : t -> int
-    val ty : t -> ty
-    val pp : t Fmt.printer
-  end
-
   module Model : sig
     type t
 
@@ -644,9 +633,9 @@ module type SOLVER = sig
 
     val mem : t -> term -> bool
 
-    val find : t -> term -> Value.t option
+    val find : t -> term -> term option
 
-    val eval : t -> term -> Value.t option
+    val eval : t -> term -> term option
 
     val pp : t Fmt.printer
   end
diff --git a/src/msat-solver/Sidekick_msat_solver.ml b/src/msat-solver/Sidekick_msat_solver.ml
index bd04e092..638ffdc0 100644
--- a/src/msat-solver/Sidekick_msat_solver.ml
+++ b/src/msat-solver/Sidekick_msat_solver.ml
@@ -561,13 +561,10 @@ module Make(A : ARG)
       | U_incomplete -> Fmt.string out "incomplete fragment"
   end [@@ocaml.warning "-37"]
 
-  (* just use terms as values *)
-  module Value = Term
-
   module Model = struct
     type t =
       | Empty
-      | Map of Value.t Term.Tbl.t
+      | Map of term Term.Tbl.t
     let empty = Empty
     let mem = function
       | Empty -> fun _ -> false
@@ -580,7 +577,7 @@ module Make(A : ARG)
       | Empty -> Fmt.string out "(model)"
       | Map tbl ->
         let pp_pair out (t,v) =
-          Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Value.pp v
+          Fmt.fprintf out "(@[<1>%a@ := %a@])" Term.pp t Term.pp v
             in
         Fmt.fprintf out "(@[<hv>model@ %a@])"
           (Util.pp_iter pp_pair) (Term.Tbl.to_iter tbl)