diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index 83a6fb199889a8f0e90f6cda76ce4744e65946b7..51672a15f04aeef9bf17c2250c35ce520158469d 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -725,7 +725,7 @@ public class MP
         	break;
             
         case EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS:
-        	b.append("TLC does not support temporal existential quantification over state variables.");
+        	b.append("TLC does not support temporal existential, nor universal, quantification over state variables.");
         	break;
         /* ************************************************************************ */
         case EC.TLC_MODULE_TLCGET_UNDEFINED:
diff --git a/tlatools/src/tlc2/tool/impl/SpecProcessor.java b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
index 5249ba9f55cc12bc325734cbb4aab8da75d94b9e..fed019f39e11ba08f7f164ac0d4c6235bdb38c22 100644
--- a/tlatools/src/tlc2/tool/impl/SpecProcessor.java
+++ b/tlatools/src/tlc2/tool/impl/SpecProcessor.java
@@ -1051,7 +1051,7 @@ public class SpecProcessor implements ValueConstants, ToolGlobals {
             }
 
             int opcode = BuiltInOPs.getOpCode(pred1.getOperator().getName());
-            if (opcode == OPCODE_te)
+            if ((opcode == OPCODE_te) || (opcode == OPCODE_tf))
             {
             	Assert.fail(EC.TLC_SPECIFICATION_FEATURES_TEMPORAL_EXISTS);
             }