diff --git a/src/lib/CoAlgLogics.ml b/src/lib/CoAlgLogics.ml
index c151b7f264913a21dd0651c12c1698003f51bb85..ee274e39e755910e1671d5bd0e7220e3d4616432 100644
--- a/src/lib/CoAlgLogics.ml
+++ b/src/lib/CoAlgLogics.ml
@@ -28,8 +28,12 @@ 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
-      bsetCopy bs
+    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
@@ -131,7 +135,7 @@ let mkRule_MultiModalKD sort bs defer sl : stateExpander =
       res
     in
     let succs = bsetMake () in (* succs := {D | ∀r.D ∈ bs *)
-    let defer1 = bsetMake () in (* TODO: actually track deferrals *)
+    let defer1 = bsetMakeRealEmpty () in (* TODO: actually track deferrals *)
     let f formula =
       if lfGetType sort formula = AxF
          && lfGetDest3 sort formula = r