diff --git a/src/transform/encoding_twin.ml b/src/transform/encoding_twin.ml
index 287a1918e28a2d975d920d4769bea20e1e944830..4d3456124ecd1dfff3cde8804e2eb5d1e0296a4f 100644
--- a/src/transform/encoding_twin.ml
+++ b/src/transform/encoding_twin.ml
@@ -46,14 +46,22 @@ let make_pont = Wty.memoize 3 (fun ty ->
     create_prop_decl Paxiom pr ax in
   t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r])
 
-let seen = Hty.create 7
+let seen_h = Hty.create 7
+let seen_q = Queue.create ()
+
+let check_in ty =
+  if not (Hty.mem seen_h ty) then begin
+    Hty.add seen_h ty ();
+    Queue.add ty seen_q
+  end
 
 let add_decls tenv decls =
-  let add ty () decls =
+  let add decls ty =
     let _,_,defs = Mty.find ty tenv in
     List.append defs decls in
-  let decls = Hty.fold add seen decls in
-  Hty.clear seen;
+  let decls = Queue.fold add decls seen_q in
+  Queue.clear seen_q;
+  Hty.clear seen_h;
   decls
 
 let conv_arg tenv t aty =
@@ -61,7 +69,7 @@ let conv_arg tenv t aty =
   if ty_equal tty aty then t else
   try
     let t2tb,tb2t,_ = Mty.find tty tenv in
-    Hty.replace seen tty ();
+    check_in tty;
     match t.t_node with
       | Tapp (fs,[t]) when ls_equal fs tb2t -> t
       | _ -> fs_app t2tb [t] tty
@@ -73,7 +81,7 @@ let conv_app tenv fs tl tty =
   if ty_equal tty vty then t else
   try
     let _,tb2t,_ = Mty.find tty tenv in
-    Hty.replace seen tty ();
+    check_in tty;
     fs_app tb2t [t] tty
   with Not_found -> t