diff --git a/dependencies/syn/src/classify.rs b/dependencies/syn/src/classify.rs
index 9d069d2fec..440ac67c20 100644
--- a/dependencies/syn/src/classify.rs
+++ b/dependencies/syn/src/classify.rs
@@ -34,8 +34,8 @@ pub(crate) fn requires_comma_to_be_match_arm(expr: &Expr) -> bool {
         | Expr::Const(_) => false,
 
         // verus
-        | Expr::Assert(e) => e.body.is_none(),
-        | Expr::AssertForall(_) => false,
+        Expr::Assert(e) => e.body.is_none(),
+        Expr::AssertForall(_) => false,
         Expr::Assume(_)
         | Expr::RevealHide(_)
         | Expr::View(_)
diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs
index 65fe66b25d..e99938c3e5 100644
--- a/dependencies/syn/src/expr.rs
+++ b/dependencies/syn/src/expr.rs
@@ -2313,6 +2313,12 @@ pub(crate) mod parsing {
             | Expr::Unsafe(_)
             | Expr::Const(_)
             | Expr::Block(_) => false,
+
+            // verus
+            Expr::Assert(e) => e.body.is_none(),
+            Expr::AssertForall(_) => false,
+            Expr::Unary(e) if matches!(e.op, crate::op::UnOp::Proof(_)) => false,
+
             _ => true,
         }
     }