diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 74e85650e5..a98dd9f075 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -1916,7 +1916,7 @@ but not `oldEnv` and the environment extension state for extensions defining `re
 `skipExisting` is true, constants that are already in `dest` are not added. If `newEnv` and `dest`
 are not derived from `oldEnv`, the result is undefined.
 -/
-def replayConsts (oldEnv newEnv : Environment) (dest : Environment) (skipExisting := false) :
+def replayConsts (dest : Environment) (oldEnv newEnv : Environment) (skipExisting := false) :
     BaseIO Environment := do
   let numNewConsts := newEnv.asyncConsts.size - oldEnv.asyncConsts.size
   let consts := newEnv.asyncConsts.revList.take numNewConsts |>.reverse