diff --git a/Frap.v b/Frap.v
index b50e9d5..cfdfc38 100644
--- a/Frap.v
+++ b/Frap.v
@@ -104,7 +104,8 @@ Ltac model_check_done :=
 
 Ltac singletoner :=
   repeat match goal with
-         | _ => apply singleton_in
+         (* | _ => apply singleton_in *)
+         | [ |- _ ?S ] => idtac S; apply singleton_in
          | [ |- (_ \cup _) _ ] => apply singleton_in_other
          end.
 
diff --git a/ModelChecking.v b/ModelChecking.v
index 04892cc..9ab1515 100644
--- a/ModelChecking.v
+++ b/ModelChecking.v
@@ -302,7 +302,8 @@ Qed.
 
 Ltac singletoner :=
   repeat match goal with
-         | _ => apply singleton_in
+         (* | _ => apply singleton_in *)
+         | [ |- _ ?S ] => idtac S; apply singleton_in
          | [ |- (_ \cup _) _ ] => apply singleton_in_other
          end.
 
@@ -1572,3 +1573,4 @@ Theorem twoadd6_ok :
 Proof.
   twoadd.
 Qed.
+