diff --git a/src/Lean/Compiler/IR/Borrow.lean b/src/Lean/Compiler/IR/Borrow.lean index cb662a557f..0bcf20f560 100644 --- a/src/Lean/Compiler/IR/Borrow.lean +++ b/src/Lean/Compiler/IR/Borrow.lean @@ -78,8 +78,7 @@ partial def visitFnBody (fnid : FunId) : FnBody → StateM ParamMap Unit | FnBody.case _ _ _ alts => alts.forM fun alt => visitFnBody fnid alt.body | e => do unless e.isTerminal do - let (_, b) := e.split - visitFnBody fnid b + visitFnBody fnid e.body def visitDecls (env : Environment) (decls : Array Decl) : StateM ParamMap Unit := decls.forM fun decl => match decl with diff --git a/src/Lean/Compiler/IR/ResetReuse.lean b/src/Lean/Compiler/IR/ResetReuse.lean index 5f0634944d..5440032f4f 100644 --- a/src/Lean/Compiler/IR/ResetReuse.lean +++ b/src/Lean/Compiler/IR/ResetReuse.lean @@ -216,8 +216,7 @@ partial def collectResets (e : FnBody) : N Unit := do | .jdecl _ _ v b => collectResets v; collectResets b | .vdecl _ _ (.reset _ x) b => modify fun s => s.insert x; collectResets b | e => unless e.isTerminal do - let (_, b) := e.split - collectResets b + collectResets e.body end ResetReuse open ResetReuse diff --git a/src/Lean/Compiler/IR/Sorry.lean b/src/Lean/Compiler/IR/Sorry.lean index afacb818e1..db2da15bb3 100644 --- a/src/Lean/Compiler/IR/Sorry.lean +++ b/src/Lean/Compiler/IR/Sorry.lean @@ -45,8 +45,7 @@ partial def visitFnBody (b : FnBody) : ExceptT Name M Unit := do | .case _ _ _ alts => alts.forM fun alt => visitFnBody alt.body | _ => unless b.isTerminal do - let (_, b) := b.split - visitFnBody b + visitFnBody b.body def visitDecl (d : Decl) : M Unit := do match d with