diff --git a/collects/redex/examples/racket-machine/verification-test.rkt b/collects/redex/examples/racket-machine/verification-test.rkt
index 3e4e1b8ed3..06b32bfc72 100644
--- a/collects/redex/examples/racket-machine/verification-test.rkt
+++ b/collects/redex/examples/racket-machine/verification-test.rkt
@@ -496,6 +496,14 @@
  (negate bytecode-ok?)
  '(let-void-box 1 (application (case-lam (lam (ref) () (loc-box-noclr 0))) (loc-noclr 1))))
 
+(test-predicate
+ (negate bytecode-ok?)
+ '(let-one 42
+           (boxenv 0
+                   (application
+                    (case-lam (lam (ref) () (loc-box 0)))
+                    (loc-box 1)))))
+
 ; literals
 (test-predicate bytecode-ok? #t)
 
diff --git a/collects/redex/examples/racket-machine/verification.rkt b/collects/redex/examples/racket-machine/verification.rkt
index 519a6a1044..89aeca13d4 100644
--- a/collects/redex/examples/racket-machine/verification.rkt
+++ b/collects/redex/examples/racket-machine/verification.rkt
@@ -108,7 +108,7 @@
    (verify (lam (τ ...) () e) s n_l b γ η f)]
   
   ; case-lam
-  [(verify (case-lam l ...) s n_l b γ η f)
+  [(verify (case-lam (name l (lam (val ...) (n ...) e)) ...) s n_l b γ η f)
    (s γ η)
    (side-condition (term (AND (verify-lam l s ?) ...)))]