diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index ee274e39e755910e1671d5bd0e7220e3d4616432..853e5aee2c0fa85e526ba99b3a6c9a31635155d2 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -27,16 +27,6 @@ let mkRuleList_MultiModalK sort bs defer sl : rule list =
   *)
   assert (List.length sl = 1);
   let refocusing = bsetCompare (bsetMakeRealEmpty ()) defer = 0 in
-  let deferral =
-    if refocusing then begin
-      print_endline ("Empty focus (Modal step) at\n" ^ (bsetToString sort bs));
-      let newdef = bsetCopy bs in
-      bsetRem newdef !S.bstrue;
-      newdef
-    end
-    else
-      defer
-  in
   let dep f bsl =                 (* dependencies for formula f (f is a diamond) *)
     assert (List.length bsl = 1); (* -+                 *)
     let bs1 = List.hd bsl in      (* -+-> [bs1] := bsl  *)
@@ -70,8 +60,8 @@ let mkRuleList_MultiModalK sort bs defer sl : rule list =
           (* if f1 = ∀R.D then bs1 = bs1 ∪ { D } *)
           let nextf1 = (lfGetDest1 sort f1) in
           bsetAdd bs1 nextf1;
-          (if (bsetMem deferral f1) &&
-                (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1) then
+          (if (refocusing && (lfGetDeferral sort nextf1) != (Hashtbl.hash "ε")) ||
+              ((bsetMem defer f1) && (lfGetDeferral sort f1) = (lfGetDeferral sort nextf1)) then
              bsetAdd defer1 nextf1;)
         else ()
       in
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 2f5fd5eeb474a7ff3f2642567967a8abb0d339b5..504a0301b718200ade206d2334f3a9e7ca8c97b8 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -891,7 +891,9 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
     raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
   else ();
   if C.HcFHt.mem vset.(s) f &&
-       compare (C.HcFHt.find vset.(s) f) deferral = 0 then ()
+    (compare (C.HcFHt.find vset.(s) f) deferral = 0) ||
+    compare deferral "ε" = 0)
+  then ()
   else
     let () = C.HcFHt.add vset.(s) f deferral in
     let () = C.HcFHt.add fset.(s) f () in