diff --git a/src/lib/dune b/src/lib/dune
index 23c57e936d..259ad44cb7 100644
--- a/src/lib/dune
+++ b/src/lib/dune
@@ -40,7 +40,7 @@
     Fun_sat Inequalities Bitv_rel Th_util Adt Adt_rel
     Instances IntervalCalculus Intervals Ite_rel Ite Matching Matching_types
     Polynome Records Records_rel Satml_frontend_hybrid Satml_frontend Satml
-    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use
+    Sat_solver Sat_solver_sig Sig Sig_rel Theory Uf Use X
     ; structures
     Commands Errors Explanation Fpa_rounding
     Parsed Profiling Satml_types Symbols
diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml
index a7d6a71232..2f1e748789 100644
--- a/src/lib/reasoners/ccx.ml
+++ b/src/lib/reasoners/ccx.ml
@@ -41,7 +41,7 @@ module type S = sig
   type t
   type r = Shostak.Combine.r
 
-  val empty : unit -> t
+  val empty : t
 
   val empty_facts : unit -> r Sig_rel.facts
 
@@ -107,9 +107,9 @@ module Main : S = struct
 
   type r = Shostak.Combine.r
 
-  let empty () = {
-    use = Use.empty ;
-    uf = Uf.empty () ;
+  let empty = {
+    use = Use.empty;
+    uf = Uf.empty;
     relation = Rel.empty [];
   }
 
diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli
index e97a9e55c8..37e4b9ced5 100644
--- a/src/lib/reasoners/ccx.mli
+++ b/src/lib/reasoners/ccx.mli
@@ -33,7 +33,7 @@ module type S = sig
   type t
   type r = Shostak.Combine.r
 
-  val empty : unit -> t
+  val empty : t
 
   val empty_facts : unit -> r Sig_rel.facts
 
diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml
index 2ad4c06bab..0920677d04 100644
--- a/src/lib/reasoners/intervalCalculus.ml
+++ b/src/lib/reasoners/intervalCalculus.ml
@@ -665,7 +665,7 @@ let empty classes = {
   improved_x = SX.empty ;
   classes = classes;
   size_splits = Q.one;
-  new_uf = Uf.empty ();
+  new_uf = Uf.empty;
 
   rat_sim =
     Sim.Solve.solve
diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml
index c8d65dbb00..7f95a43f31 100644
--- a/src/lib/reasoners/theory.ml
+++ b/src/lib/reasoners/theory.ml
@@ -712,7 +712,7 @@ module Main_Default : S = struct
     else {env with gamma=gm; gamma_finite=add_term_in_gm env.gamma_finite t}
 
   let empty () =
-    let env = CC_X.empty () in
+    let env = CC_X.empty in
     let env, _ = CC_X.add_term env (CC_X.empty_facts()) E.vrai Ex.empty in
     let env, _ = CC_X.add_term env (CC_X.empty_facts()) E.faux Ex.empty in
     let t =
@@ -798,9 +798,8 @@ module Main_Empty : S = struct
   let cl_extract _ = []
   let extract_ground_terms _ = Expr.Set.empty
 
-  let empty_ccx = CC_X.empty ()
-  let get_real_env _ = empty_ccx
-  let get_case_split_env _ = empty_ccx
+  let get_real_env _ = CC_X.empty
+  let get_case_split_env _ = CC_X.empty
   let do_case_split env _ = env, E.Set.empty
   let add_term env _ ~add_in_cs:_ = env
   let compute_concrete_model _env = None
diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index f1d7ddb768..5663665d7a 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -28,8 +28,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-module X = Shostak.Combine
-
 module Ac = Shostak.Ac
 module Ex = Explanation
 
@@ -900,7 +898,7 @@ let term_repr uf t =
   try SE.min_elt st
   with Not_found -> t
 
-let empty () =
+let empty =
   let env = {
     make  = ME.empty;
     repr = MapX.empty;
@@ -912,7 +910,7 @@ let empty () =
   in
   let env, _ = add env E.vrai in
   let env, _ = add env E.faux in
-  distinct env [X.top (); X.bot ()] Ex.empty
+  distinct env [X.top; X.bot] Ex.empty
 
 let make uf t = ME.find t uf.make
 
diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli
index e6e6d7f738..fbe39d00ce 100644
--- a/src/lib/reasoners/uf.mli
+++ b/src/lib/reasoners/uf.mli
@@ -36,7 +36,7 @@ type r = Shostak.Combine.r
 
 module LX : Xliteral.S with type elt = r
 
-val empty : unit -> t
+val empty : t
 val add : t -> Expr.t -> t * Expr.t list
 
 val mem : t -> Expr.t -> bool
diff --git a/src/lib/reasoners/x.ml b/src/lib/reasoners/x.ml
new file mode 100644
index 0000000000..d036163f39
--- /dev/null
+++ b/src/lib/reasoners/x.ml
@@ -0,0 +1,4 @@
+include Shostak.Combine
+
+let top = top ()
+let bot = bot ()
diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml
index 4f2871a1e4..cbfd459610 100644
--- a/src/lib/structures/xliteral.ml
+++ b/src/lib/structures/xliteral.ml
@@ -49,8 +49,8 @@ module type OrderedType = sig
   val compare : t -> t -> int
   val hash :  t -> int
   val print : Format.formatter -> t -> unit
-  val top : unit -> t
-  val bot : unit -> t
+  val top : t
+  val bot : t
   val type_info : t -> Ty.t
 end
 
@@ -231,16 +231,16 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
   module HC = Hconsing.Make(V)
 
   let normalize_eq_bool t1 t2 is_neg =
-    if X.compare t1 (X.bot()) = 0 then Pred(t2, not is_neg)
-    else if X.compare t2 (X.bot()) = 0 then Pred(t1, not is_neg)
-    else if X.compare t1 (X.top()) = 0 then Pred(t2, is_neg)
-    else if X.compare t2 (X.top()) = 0 then Pred(t1, is_neg)
+    if X.compare t1 (X.bot) = 0 then Pred(t2, not is_neg)
+    else if X.compare t2 (X.bot) = 0 then Pred(t1, not is_neg)
+    else if X.compare t1 (X.top) = 0 then Pred(t2, is_neg)
+    else if X.compare t2 (X.top) = 0 then Pred(t1, is_neg)
     else if is_neg then Distinct (false, [t1;t2]) (* XXX assert ? *)
     else Eq(t1,t2) (* should be translated into iff *)
 
   let normalize_eq t1 t2 is_neg =
     let c = X.compare t1 t2 in
-    if c = 0 then Pred(X.top(), is_neg)
+    if c = 0 then Pred(X.top, is_neg)
     else
       let t1, t2 = if c < 0 then t1, t2 else t2, t1 in
       if X.type_info t1 == Ty.Tbool then normalize_eq_bool t1 t2 is_neg
@@ -273,15 +273,15 @@ module Make (X : OrderedType) : S with type elt = X.t = struct
 
   (*
     let mk_eq_bool t1 t2 is_neg =
-    if X.compare t1 (X.bot()) = 0 then make_aux (PR t2) (not is_neg)
-    else if X.compare t2 (X.bot()) = 0 then make_aux (PR t1) (not is_neg)
-    else if X.compare t1 (X.top()) = 0 then make_aux (PR t2) is_neg
-    else if X.compare t2 (X.top()) = 0 then make_aux (PR t1) is_neg
+    if X.compare t1 (X.bot) = 0 then make_aux (PR t2) (not is_neg)
+    else if X.compare t2 (X.bot) = 0 then make_aux (PR t1) (not is_neg)
+    else if X.compare t1 (X.top) = 0 then make_aux (PR t2) is_neg
+    else if X.compare t2 (X.top) = 0 then make_aux (PR t1) is_neg
     else make_aux (EQ(t1,t2)) is_neg
 
     let mk_equa t1 t2 is_neg =
     let c = X.compare t1 t2 in
-    if c = 0 then make_aux (PR (X.top())) is_neg
+    if c = 0 then make_aux (PR (X.top)) is_neg
     else
     let t1, t2 = if c < 0 then t1, t2 else t2, t1 in
     if X.type_info t1 = Ty.Tbool then mk_eq_bool t1 t2 is_neg
diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli
index ccb1734636..84d5f46ecd 100644
--- a/src/lib/structures/xliteral.mli
+++ b/src/lib/structures/xliteral.mli
@@ -52,8 +52,8 @@ module type OrderedType = sig
   val compare : t -> t -> int
   val hash :  t -> int
   val print : Format.formatter -> t -> unit
-  val top : unit -> t
-  val bot : unit -> t
+  val top : t
+  val bot : t
   val type_info : t -> Ty.t
 end