diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 57af386387..efcbf1b74d 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -130,12 +130,15 @@ where
   generateElements (numArgs : Array Nat) (argCombination : Array Nat) : TermElabM (Array TerminationByElement) := do
     let mut result := #[]
     let var ← `(x)
-    let body ← `(sizeOf x)
     let hole ← `(_)
-    for preDef in preDefs, numArg in numArgs, argIdx in argCombination do
+    for preDef in preDefs, numArg in numArgs, argIdx in argCombination, i in [:preDefs.size] do
       let mut vars := #[var]
       for i in [:numArg - argIdx - 1] do
         vars := vars.push hole
+      -- TODO: improve this.
+      -- The following trick allows a function `f` in a mutual block to invoke `g` appearing before it with the input argument.
+      -- We should compute the "right" order (if there is one) in the future.
+      let body ← `((sizeOf x, $(quote i)))
       result := result.push {
         ref := preDef.ref
         declName := preDef.declName
diff --git a/tests/lean/run/lex.lean b/tests/lean/run/lex.lean
index 9d326ac1f1..561c6f1262 100644
--- a/tests/lean/run/lex.lean
+++ b/tests/lean/run/lex.lean
@@ -66,10 +66,6 @@ mutual
           | .error _ => return { text := { data := text.reverse }, tok := Tok.num soFar } :: (← lex2 (c::cs)) -- Use `c::cs` here instead of `input` because the default tactic doesn't know they are equal.
           | .ok d => lex2number (soFar * 10 + d) (c :: text) cs
 end
--- `termination_by` is used to specify a well-founded relation.
-termination_by
-  lex2 input       => (input, 0) -- Lean is proving a termination using the instance `WellFoundedRelation (List Char × Nat)` which is just a lex-order. In the future, we should be able to guess this too.
-  lex2number input => (input, 1)
 
 #eval lex2 (m := Except LexErr) "".data
 #eval lex2 (m := Except LexErr) "123".data
@@ -131,9 +127,6 @@ mutual
           | .error _ => return { text := { data := text.reverse }, tok := Tok.num soFar } :: (← lex4 input)
           | .ok d => lex4number (soFar * 10 + d) (c :: text) cs
 end
-termination_by
-  lex4 input       => (input, 0) -- Lean is proving a termination using the instance `WellFoundedRelation (List Char × Nat)` which is just a lex-order. In the future, we should be able to guess this too.
-  lex4number input => (input, 1)
 -- decreasing_by allows us to specify a tactic for showing the recursive applications are decreasing.
 decreasing_by
   solve | decreasing_tactic -- get easy cases with the builtin tactic `decreasing_tactic`
@@ -210,9 +203,6 @@ mutual
     else
       return [{ text := text.reverse.asString, tok := Tok.num soFar }]
 end
-termination_by
-  lex input       => (input, 0)
-  lexnumber input => (input, 1)
 
 #eval lex (m := Except LexErr) "".iter
 #eval lex (m := Except LexErr) "123".iter