diff --git a/smt/smt.ml b/smt/smt.ml
index 873cfcf4..963e0af7 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -5,6 +5,7 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Fsmt = Expr
+module ThI = Theory_intf
 
 module Tsmt = struct
 
@@ -12,12 +13,6 @@ module Tsmt = struct
 
   type formula = Fsmt.t
   type proof = unit
-  type slice = {
-    start : int;
-    length : int;
-    get : int -> formula;
-    push : formula list -> proof -> unit;
-  }
   type level = CC.t
 
   type res =
@@ -43,9 +38,9 @@ module Tsmt = struct
 
   let assume s =
     try
-      for i = s.start to s.start + s.length - 1 do
-        Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.get i));
-        match s.get i with
+      for i = s.ThI.start to s.ThI.start + s.ThI.length - 1 do
+        Log.debugf 10 "Propagating in th :@ @[%a@]" (fun k->k Fsmt.print (s.ThI.get i));
+        match s.ThI.get i with
         | Fsmt.Prop _ -> ()
         | Fsmt.Equal (i, j) -> env := CC.add_eq !env i j
         | Fsmt.Distinct (i, j) -> env := CC.add_neq !env i j
diff --git a/solver/solver.ml b/solver/solver.ml
index 3a34f089..c0cef30a 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -11,6 +11,7 @@
 (**************************************************************************)
 
 module type S = Solver_intf.S
+module ThI = Theory_intf
 
 module DummyTheory(F : Formula_intf.S) = struct
   (* We don't have anything to do since the SAT Solver already
@@ -75,10 +76,11 @@ module Plugin(E : Formula_intf.S)
 
   let assume s =
     match Th.assume {
-        Th.start = s.start;
-        Th.length = s.length;
-        Th.get = assume_get s;
-        Th.push = s.push;
+        ThI.
+        start = s.start;
+        length = s.length;
+        get = assume_get s;
+        push = s.push;
       } with
     | Th.Sat _ -> Sat
     | Th.Unsat (l, p) -> Unsat (l, p)
diff --git a/solver/theory_intf.ml b/solver/theory_intf.ml
index 527b73b1..01d16d02 100644
--- a/solver/theory_intf.ml
+++ b/solver/theory_intf.ml
@@ -18,6 +18,9 @@ type ('form, 'proof) slice = {
   get : int -> 'form;
   push : 'form list -> 'proof -> unit;
 }
+(** The type for a slice of literals to assume/propagate in the theory.
+    [get] operations should only be used for integers [ start <= i < start + length].
+    [push clause proof] allows to add a tautological clause to the sat solver. *)
 
 module type S = sig
   (** Signature for theories to be given to the Solver. *)
@@ -28,16 +31,6 @@ module type S = sig
   type proof
   (** A custom type for the proofs of lemmas produced by the theory. *)
 
-  type slice = {
-    start : int;
-    length : int;
-    get : int -> formula;
-    push : formula list -> proof -> unit;
-  }
-  (** The type for a slice of literals to assume/propagate in the theory.
-      [get] operations should only be used for integers [ start <= i < start + length].
-      [push clause proof] allows to add a tautological clause to the sat solver. *)
-
   type level
   (** The type for levels to allow backtracking. *)
 
@@ -56,7 +49,7 @@ module type S = sig
   (** Return the current level of the theory (either the empty/beginning state, or the
       last level returned by the [assume] function). *)
 
-  val assume : slice -> res
+  val assume : (formula, proof) slice -> res
   (** Assume the formulas in the slice, possibly pushing new formulas to be propagated,
       and returns the result of the new assumptions. *)