diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index f975167c3ed1ce7d62f033431e29a6d1c1fa077a..0e792d0961dc2f5725e360d7578947725e80e8b5 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -38,7 +38,6 @@ let occurs xs a = Vars.intersect xs (F.vars a)
 module Ground =
 struct
 
-  type subst = pred -> pred
   type env = {
     mutable ground : bool Tmap.t ;
     sigma : F.sigma ;
@@ -125,11 +124,6 @@ struct
   let top () = { ground = Tmap.empty ; sigma = Lang.sigma () }
   let copy env = { ground = env.ground ; sigma = Subst.copy env.sigma }
 
-  let singleton p =
-    let env = top () in
-    ignore (assume env p) ;
-    p_apply env
-
   let branch env p =
     let p = p_apply env p in
     let wa = copy env in
diff --git a/src/plugins/wp/Letify.mli b/src/plugins/wp/Letify.mli
index 2f3d146ed9e849f9395789271dda78625d8c905a..5e32818fe2e602d5a39ef67010d2a897105b6788 100644
--- a/src/plugins/wp/Letify.mli
+++ b/src/plugins/wp/Letify.mli
@@ -29,9 +29,6 @@ open Lang.F
 module Ground :
 sig
 
-  type subst = pred -> pred
-  val singleton : pred -> subst
-
   type env
   val top : unit -> env
   val copy : env -> env