diff --git a/README.md b/README.md
index 620e33fc..43eed5df 100644
--- a/README.md
+++ b/README.md
@@ -23,7 +23,7 @@ as shown in the following code :
 ```ocaml
     (* Module initialization *)
     module F = Msat.Sat.Tseitin
-    module Sat = Msat.Sat.Make(Msat.Log)
+    module Sat = Msat.Sat.Make()
 
     (* We create here two distinct atoms *)
     let a = Sat.new_atom () (* A 'new_atom' is always distinct from any other atom *)
diff --git a/_tags b/_tags
index 26f4f35a..2ea41d17 100644
--- a/_tags
+++ b/_tags
@@ -6,10 +6,10 @@
 <backend/*.cmx>: for-pack(Msat)
 
 # enable stronger inlining everywhere
-#<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
-#<solver/*.cmx>: inline(50)
-#<sat/**/*.cmx>: inline(100)
-#<smt/**/*.cmx>: inline(100)
+<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
+<solver/*.cmx>: inline(50)
+<sat/**/*.cmx>: inline(100)
+<smt/**/*.cmx>: inline(100)
 <util/log.cmx>: inline(30)
 
 # more warnings
diff --git a/sat/sat.ml b/sat/sat.ml
index 5460fe8d..9f6a3070 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -66,7 +66,7 @@ module Tseitin = Tseitin.Make(Fsat)
 module Make(Dummy : sig end) = struct
 
   module Tsat = Solver.DummyTheory(Fsat)
-  include Solver.Make(Fsat)(Tsat)
+  include Solver.Make(Fsat)(Tsat)()
 
   let print_atom = Fsat.print
   let print_clause = St.print_clause
diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index 254f32e6..04cd779f 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -111,7 +111,7 @@ end
 
 module Make(Dummy:sig end) = struct
 
-  module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)
+  module SmtSolver = Mcsolver.Make(Fsmt)(Tsmt)()
 
   module Proof = SmtSolver.Proof
 
diff --git a/smt/smt.ml b/smt/smt.ml
index 1248fd57..af29e57b 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -61,7 +61,7 @@ end
 
 module Make(Dummy:sig end) = struct
 
-  include Solver.Make(Fsmt)(Tsmt)
+  include Solver.Make(Fsmt)(Tsmt)()
   module Dot = Dot.Make(Proof)(struct
       let clause_name c = St.(c.name)
       let print_atom = St.print_atom
diff --git a/solver/internal.ml b/solver/internal.ml
index 6b4b8a8b..318826b6 100644
--- a/solver/internal.ml
+++ b/solver/internal.ml
@@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes
 module Make
     (St : Solver_types.S)
     (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
+    (Dummy: sig end)
 = struct
 
   module Proof = Res.Make(St)
diff --git a/solver/internal.mli b/solver/internal.mli
index c00f5eaf..189f1d80 100644
--- a/solver/internal.mli
+++ b/solver/internal.mli
@@ -7,6 +7,7 @@ Copyright 2014 Simon Cruanes
 module Make
   (St : Solver_types.S)
   (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
+  (Dummy: sig end)
 : sig
   (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
 
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index f50d6c7d..c3358a1a 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -5,11 +5,12 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make (E : Expr_intf.S)
-    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) = struct
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof)
+    (Dummy: sig end) = struct
 
   module St = Solver_types.McMake(E)
 
-  module M = Internal.Make(St)(Th)
+  module M = Internal.Make(St)(Th)()
 
   include St
 
diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli
index 26a0e92a..1bcc48d0 100644
--- a/solver/mcsolver.mli
+++ b/solver/mcsolver.mli
@@ -5,7 +5,8 @@ Copyright 2014 Simon Cruanes
 *)
 
 module Make (E : Expr_intf.S)
-    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof) : sig
+    (Th : Plugin_intf.S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof)
+    (Dummy: sig end) : sig
   (** Functor to create a solver parametrised by the atomic formulas and a theory. *)
 
   exception Unsat
diff --git a/solver/solver.ml b/solver/solver.ml
index c4207662..2481fa65 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -99,13 +99,14 @@ end
 
 
 module Make (E : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = E.t and type proof = E.proof) = struct
+    (Th : Theory_intf.S with type formula = E.t and type proof = E.proof)
+    (Dummy: sig end) = struct
 
   module P = Plugin(E)(Th)
 
   module St = Solver_types.SatMake(E)
 
-  module S = Internal.Make(St)(P)
+  module S = Internal.Make(St)(P)()
 
   module Proof = S.Proof
 
diff --git a/solver/solver.mli b/solver/solver.mli
index 8d705aa9..70793d58 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -18,7 +18,8 @@ module DummyTheory(F : Formula_intf.S with type proof = unit) :
   Theory_intf.S with type formula = F.t and type proof = unit
 
 module Make (F : Formula_intf.S)
-    (Th : Theory_intf.S with type formula = F.t and type proof = F.proof) :
+    (Th : Theory_intf.S with type formula = F.t and type proof = F.proof)
+    (Dummy: sig end) :
   S with type St.formula = F.t
      and type St.proof = F.proof
   (** Functor to create a SMT Solver parametrised by the atomic