diff --git a/src/Lean/Compiler/IR/Boxing.lean b/src/Lean/Compiler/IR/Boxing.lean
index d199c88027..0f3f66c4ac 100644
--- a/src/Lean/Compiler/IR/Boxing.lean
+++ b/src/Lean/Compiler/IR/Boxing.lean
@@ -21,13 +21,8 @@ Recall that the Lean to λ_pure compiler produces code without these instruction
 
 Assumptions:
 - This transformation is applied before explicit RC instructions (`inc`, `dec`) are inserted.
-- This transformation is applied before `FnBody.case` has been simplified and `Alt.default` is used.
-  Reason: if there is no `Alt.default` branch, then we can decide whether `x` at `FnBody.case x alts` is an
-  enumeration type by simply inspecting the `CtorInfo` values at `alts`.
 - This transformation is applied before lower level optimizations are applied which use
   `Expr.isShared`, `Expr.isTaggedPtr`, and `FnBody.set`.
-- This transformation is applied after `reset` and `reuse` instructions have been added.
-  Reason: `resetreuse.lean` ignores `box` and `unbox` instructions.
 -/
 
 def mkBoxedName (n : Name) : Name :=