diff --git a/RELEASES.md b/RELEASES.md
index a2d912f10c..e2c2e1e72f 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -20,6 +20,22 @@ v4.5.0 (development in progress)
   ```
   [PR #2821](https://github.com/leanprover/lean4/pull/2821) and [RFC #2838](https://github.com/leanprover/lean4/issues/2838).
 
+* The low-level `termination_by'` clause is no longer supported.
+
+  Migration guide: Use `termination_by` instead, e.g.:
+  ```diff
+  -termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+  +termination_by go i _ => as.size - i
+  ```
+
+  If the well-founded relation you want to use is not the one that the
+  `WellFoundedRelation` type class would infer for your termination argument,
+  you can use `WellFounded.wrap` from the std libarary to explicitly give one:
+  ```diff
+  -termination_by' ⟨r, hwf⟩
+  +termination_by _ x => hwf.wrap x
+  ```
+
 v4.4.0
 ---------
 
diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean
index 0e458ae908..bc89dc993f 100644
--- a/src/Lean/Elab/PreDefinition/Main.lean
+++ b/src/Lean/Elab/PreDefinition/Main.lean
@@ -100,8 +100,8 @@ def addPreDefinitions (preDefs : Array PreDefinition) (hints : TerminationHints)
   let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef
   let preDefs ← betaReduceLetRecApps preDefs
   let cliques := partitionPreDefs preDefs
-  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
-  let mut decreasingBy  ← liftMacroM <| WF.expandTerminationHint hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
+  let mut terminationBy ← liftMacroM <| WF.expandTerminationBy? hints.terminationBy? (cliques.map fun ds => ds.map (·.declName))
+  let mut decreasingBy  ← liftMacroM <| WF.expandDecreasingBy? hints.decreasingBy? (cliques.map fun ds => ds.map (·.declName))
   let mut hasErrors := false
   for preDefs in cliques do
     trace[Elab.definition.scc] "{preDefs.map (·.declName)}"
diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
index 3dbe2ec4fa..14a1c8773f 100644
--- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
+++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean
@@ -32,7 +32,6 @@ In addition to measures derived from `sizeOf xᵢ`, it also considers measures
 that assign an order to the functions themselves. This way we can support mutual
 function definitions where no arguments decrease from one function to another.
 
-
 The result of this module is a `TerminationWF`, which is then passed on to `wfRecursion`; this
 design is crucial so that whatever we infer in this module could also be written manually by the
 user. It would be bad if there are function definitions that can only be processed with the
@@ -590,7 +589,7 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
         declName, vars, body,
         implicit := true
       }
-  return .ext termByElements
+  return termByElements
 
 
 /--
diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean
index 6ca0bd16ea..3b21f175ed 100644
--- a/src/Lean/Elab/PreDefinition/WF/Rel.lean
+++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean
@@ -34,10 +34,10 @@ private partial def unpackUnary (preDef : PreDefinition) (prefixSize : Nat) (mva
     let mut varNames ← xs.mapM fun x => x.fvarId!.getUserName
     if element.vars.size > varNames.size then
       throwErrorAt element.vars[varNames.size]! "too many variable names"
-    for i in [:element.vars.size] do
-      let varStx := element.vars[i]!
-      if varStx.isIdent then
-        varNames := varNames.set! (varNames.size - element.vars.size + i) varStx.getId
+    for h : i in [:element.vars.size] do
+      let varStx := element.vars[i]'h.2
+      if let `($ident:ident) := varStx then
+        varNames := varNames.set! (varNames.size - element.vars.size + i) ident.getId
     return varNames
   let mut mvarId := mvarId
   for localDecl in (← Term.getMVarDecl mvarId).lctx, varName in varNames[:prefixSize] do
@@ -60,25 +60,18 @@ def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (fixedPre
   let expectedType := mkApp (mkConst ``WellFoundedRelation [u]) α
   trace[Elab.definition.wf] "elabWFRel start: {(← mkFreshTypeMVar).mvarId!}"
   withDeclName unaryPreDefName do
-  match wf with
-  | TerminationWF.core wfStx =>
-      let wfRel ← instantiateMVars (← withSynthesize <| elabTermEnsuringType wfStx expectedType)
-      let pendingMVarIds ← getMVars wfRel
-      discard <| logUnassignedUsingErrorInfos pendingMVarIds
-      k wfRel
-  | TerminationWF.ext elements =>
-    withRef (getRefFromElems elements) do
-      let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
-      let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
-      let (d, fMVarId) ← fMVarId.intro1
-      let subgoals ← unpackMutual preDefs fMVarId d
-      for (d, mvarId) in subgoals, element in elements, preDef in preDefs do
-        let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
-        mvarId.withContext do
-          let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
-          mvarId.assign value
-      let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
-      wfRelMVarId.assign wfRelVal
-      k (← instantiateMVars (mkMVar mainMVarId))
+  withRef (getRefFromElems wf) do
+    let mainMVarId := (← mkFreshExprSyntheticOpaqueMVar expectedType).mvarId!
+    let [fMVarId, wfRelMVarId, _] ← mainMVarId.apply (← mkConstWithFreshMVarLevels ``invImage) | throwError "failed to apply 'invImage'"
+    let (d, fMVarId) ← fMVarId.intro1
+    let subgoals ← unpackMutual preDefs fMVarId d
+    for (d, mvarId) in subgoals, element in wf, preDef in preDefs do
+      let mvarId ← unpackUnary preDef fixedPrefixSize mvarId d element
+      mvarId.withContext do
+        let value ← Term.withSynthesize <| elabTermEnsuringType element.body (← mvarId.getType)
+        mvarId.assign value
+    let wfRelVal ← synthInstance (← inferType (mkMVar wfRelMVarId))
+    wfRelMVarId.assign wfRelVal
+    k (← instantiateMVars (mkMVar mainMVarId))
 
 end Lean.Elab.WF
diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
index 3c2dd4cafd..b7d54f051c 100644
--- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
+++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
@@ -5,44 +5,46 @@ Authors: Leonardo de Moura
 -/
 import Lean.Parser.Command
 
+set_option autoImplicit false
+
 namespace Lean.Elab.WF
 
-/-! # Support for `decreasing_by` and `termination_by'` notations -/
+/-! # Support for `decreasing_by` -/
 
-structure TerminationHintValue where
+structure DecreasingByTactic where
   ref   : Syntax
-  value : Syntax
+  value : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq
   deriving Inhabited
 
-inductive TerminationHint where
+inductive DecreasingBy where
   | none
-  | one (val : TerminationHintValue)
-  | many (map : NameMap TerminationHintValue)
+  | one (val : DecreasingByTactic)
+  | many (map : NameMap DecreasingByTactic)
   deriving Inhabited
 
 open Parser.Command in
 /--
-This function takes a user-specified `decreasing_by` or `termination_by'` clause (as `Sytnax`).
-If it is a `terminathionHintMany` (a set of clauses guarded by the function name) then
+This function takes a user-specified `decreasing_by` clause (as `Sytnax`).
+If it is a `decreasingByMany` (a set of clauses guarded by the function name) then
 * checks that all mentioned names exist in the current declaration
 * check that at most one function from each clique is mentioned
 and sort the entries by function name.
 -/
-def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationHint := do
-  let some terminationHint := terminationHint? | return TerminationHint.none
-  let ref := terminationHint
-  match terminationHint with
-  | `(terminationByCore|termination_by' $hint1:terminationHint1)
-  | `(decreasingBy|decreasing_by $hint1:terminationHint1) =>
-    return TerminationHint.one { ref, value := hint1.raw[0] }
-  | `(terminationByCore|termination_by' $hints:terminationHintMany)
-  | `(decreasingBy|decreasing_by $hints:terminationHintMany) => do
-    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg =>
+def expandDecreasingBy? (decreasingBy? : Option Syntax) (cliques : Array (Array Name)) : MacroM DecreasingBy := do
+  let some decreasingBy := decreasingBy? | return DecreasingBy.none
+  let ref := decreasingBy
+  match decreasingBy with
+  | `(decreasingBy|decreasing_by $hint1:tacticSeq) =>
+    return DecreasingBy.one { ref, value := hint1 }
+  | `(decreasingBy|decreasing_by $hints:decreasingByMany) => do
+    let m ← hints.raw[0].getArgs.foldlM (init := {}) fun m arg => do
+      let arg : TSyntax `decreasingByElement := ⟨arg⟩ -- cannot use syntax pattern match with lookahead
+      let `(decreasingByElement| $declId:ident => $tac:tacticSeq) := arg | Macro.throwUnsupported
       let declName? := cliques.findSome? fun clique => clique.findSome? fun declName =>
-        if arg[0].getId.isSuffixOf declName then some declName else none
+        if declId.getId.isSuffixOf declName then some declName else none
       match declName? with
-      | none => Macro.throwErrorAt arg[0] s!"function '{arg[0].getId}' not found in current declaration"
-      | some declName => return m.insert declName { ref := arg, value := arg[2] }
+      | none => Macro.throwErrorAt declId s!"function '{declId.getId}' not found in current declaration"
+      | some declName => return m.insert declName { ref := arg, value := tac }
     for clique in cliques do
       let mut found? := Option.none
       for declName in clique do
@@ -50,69 +52,65 @@ def expandTerminationHint (terminationHint? : Option Syntax) (cliques : Array (A
           if let some found := found? then
             Macro.throwErrorAt ref s!"invalid termination hint element, '{declName}' and '{found}' are in the same clique"
           found? := some declName
-    return TerminationHint.many m
+    return DecreasingBy.many m
   | _ => Macro.throwUnsupported
 
-def TerminationHint.markAsUsed (t : TerminationHint) (clique : Array Name) : TerminationHint :=
+def DecreasingBy.markAsUsed (t : DecreasingBy) (clique : Array Name) : DecreasingBy :=
   match t with
-  | TerminationHint.none   => TerminationHint.none
-  | TerminationHint.one .. => TerminationHint.none
-  | TerminationHint.many m => Id.run do
+  | DecreasingBy.none   => DecreasingBy.none
+  | DecreasingBy.one .. => DecreasingBy.none
+  | DecreasingBy.many m => Id.run do
     for declName in clique do
       if m.contains declName then
         let m := m.erase declName
         if m.isEmpty then
-          return TerminationHint.none
+          return DecreasingBy.none
         else
-          return TerminationHint.many m
+          return DecreasingBy.many m
     return t
 
-def TerminationHint.find? (t : TerminationHint) (clique : Array Name) : Option TerminationHintValue :=
+def DecreasingBy.find? (t : DecreasingBy) (clique : Array Name) : Option DecreasingByTactic :=
   match t with
-  | TerminationHint.none   => Option.none
-  | TerminationHint.one v  => some v
-  | TerminationHint.many m => clique.findSome? m.find?
+  | DecreasingBy.none   => Option.none
+  | DecreasingBy.one v  => some v
+  | DecreasingBy.many m => clique.findSome? m.find?
 
-def TerminationHint.ensureAllUsed (t : TerminationHint) : MacroM Unit := do
+def DecreasingBy.ensureAllUsed (t : DecreasingBy) : MacroM Unit := do
   match t with
-  | TerminationHint.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
-  | TerminationHint.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
+  | DecreasingBy.one v   => Macro.throwErrorAt v.ref "unused termination hint element"
+  | DecreasingBy.many m  => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
   | _ => pure ()
 
-/-! # Support for `termination_by` and `termination_by'` notation -/
+/-! # Support for `termination_by` notation -/
 
 /-- A single `termination_by` clause -/
 structure TerminationByElement where
   ref       : Syntax
   declName  : Name
-  vars      : Array Syntax
-  body      : Syntax
+  vars      : TSyntaxArray [`ident, ``Lean.Parser.Term.hole]
+  body      : Term
   implicit  : Bool
   deriving Inhabited
 
-/-- `terminatoin_by` clauses, grouped by clique -/
+/-- `termination_by` clauses, grouped by clique -/
 structure TerminationByClique where
   elements : Array TerminationByElement
   used     : Bool := false
 
 /--
-A `termination_by'` or `termination_by` hint, as specified by the user
+A `termination_by` hint, as specified by the user
 -/
-inductive TerminationBy where
-  /-- `termination_by'` -/
-  | core (hint : TerminationHint)
-  /-- `termination_by` -/
-  | ext  (cliques : Array TerminationByClique)
+structure TerminationBy where
+  cliques : Array TerminationByClique
   deriving Inhabited
 
 /--
-A `termination_by'` or `termination_by` hint, as applicable to a single clique
+A `termination_by` hint, as applicable to a single clique
 -/
-inductive TerminationWF where
-  | core (stx : Syntax)
-  | ext  (clique : Array TerminationByElement)
+abbrev TerminationWF := Array TerminationByElement
 
-/-
+open Parser.Command in
+/--
 Expands the syntax for a `termination_by` clause, checking that
 * each function is mentioned once
 * each function mentioned actually occurs in the current declaration
@@ -125,8 +123,9 @@ def terminationByElement   := leading_parser ppLine >> (ident <|> hole) >> many
 def terminationBy          := leading_parser ppLine >> "termination_by " >> many1chIndent terminationByElement
 ```
 -/
-open Parser.Command in
-private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy := do
+def expandTerminationBy? (hint? : Option Syntax) (cliques : Array (Array Name)) :
+    MacroM TerminationBy := do
+  let some hint := hint?  | return { cliques := #[] }
   let `(terminationBy|termination_by $elementStxs*) := hint | Macro.throwUnsupported
   let mut alreadyFound : NameSet := {}
   let mut elseElemStx? := none
@@ -170,51 +169,28 @@ private def expandTerminationByNonCore (hint : Syntax) (cliques : Array (Array N
       result := result.push { elements }
   if !usedElse && elseElemStx?.isSome then
     withRef elseElemStx?.get! <| Macro.throwError s!"invalid `termination_by` syntax, unnecessary else-case"
-  return TerminationBy.ext result
-
-/--
-Expands the syntax for a `termination_by` or `termination_by'` clause, using the appropriate function
--/
-def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) : MacroM TerminationBy :=
-  if let some hint := hint? then
-    if hint.isOfKind ``Parser.Command.terminationByCore then
-      return TerminationBy.core (← expandTerminationHint hint? cliques)
-    else if hint.isOfKind ``Parser.Command.terminationBy then
-      expandTerminationByNonCore hint cliques
-    else
-      Macro.throwUnsupported
-  else
-      return TerminationBy.core TerminationHint.none
+  return ⟨result⟩
 
 open Parser.Command in
-def TerminationWF.unexpand : TerminationWF → MetaM Syntax
-  | .ext elements => do
-    let elementStxs ← elements.mapM fun element => do
-      let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
-      let body : Term := ⟨element.body⟩
-      let vars : Array Ident := element.vars.map TSyntax.mk
-      `(terminationByElement|$fn $vars* => $body)
-    `(terminationBy|termination_by $elementStxs*)
-  | .core _ => unreachable! -- we don't synthetize termination_by' syntax
+def TerminationWF.unexpand (elements : TerminationWF) : MetaM Syntax := do
+  let elementStxs ← elements.mapM fun element => do
+    let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
+    `(terminationByElement|$fn $element.vars* => $element.body)
+  `(terminationBy|termination_by $elementStxs*)
 
 def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
-  match t with
-  | core hint   => core (hint.markAsUsed cliqueNames)
-  | ext cliques => ext <| cliques.map fun clique =>
+  .mk <| t.cliques.map fun clique =>
     if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
       { clique with used := true }
     else
       clique
 
 def TerminationBy.find? (t : TerminationBy) (cliqueNames : Array Name) : Option TerminationWF :=
-  match t with
-  | core hint => hint.find? cliqueNames |>.map fun v => TerminationWF.core v.value
-  | ext cliques =>
-    cliques.findSome? fun clique =>
-      if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
-        some <| TerminationWF.ext clique.elements
-      else
-        none
+  t.cliques.findSome? fun clique =>
+    if cliqueNames.any fun name => clique.elements.any fun elem => elem.declName == name then
+      some <| clique.elements
+    else
+      none
 
 def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
   c.elements.all fun elem => elem.implicit
@@ -222,19 +198,16 @@ def TerminationByClique.allImplicit (c : TerminationByClique) : Bool :=
 def TerminationByClique.getExplicitElement? (c : TerminationByClique) : Option TerminationByElement :=
   c.elements.find? (!·.implicit)
 
-def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit :=
-  match t with
-  | core hint => hint.ensureAllUsed
-  | ext cliques => do
-    let hasUsedAllImplicit := cliques.any fun c => c.allImplicit && c.used
-    let mut reportedAllImplicit := true
-    for clique in cliques do
-      unless clique.used do
-        if let some explicitElem := clique.getExplicitElement? then
-          Macro.throwErrorAt explicitElem.ref "unused termination hint element"
-        else if !hasUsedAllImplicit then
-          unless reportedAllImplicit do
-            reportedAllImplicit := true
-            Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
+def TerminationBy.ensureAllUsed (t : TerminationBy) : MacroM Unit := do
+  let hasUsedAllImplicit := t.cliques.any fun c => c.allImplicit && c.used
+  let mut reportedAllImplicit := true
+  for clique in t.cliques do
+    unless clique.used do
+      if let some explicitElem := clique.getExplicitElement? then
+        Macro.throwErrorAt explicitElem.ref "unused termination hint element"
+      else if !hasUsedAllImplicit then
+        unless reportedAllImplicit do
+          reportedAllImplicit := true
+          Macro.throwErrorAt clique.elements[0]!.ref "unused termination hint element"
 
 end Lean.Elab.WF
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 3b1c83272d..4d2981dd80 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -28,23 +28,18 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
-/-
-A mutual block may be broken in different cliques,
-we identify them using an `ident` (an element of the clique).
-We provide two kinds of hints to the termination checker:
-1- A wellfounded relation (`p` is `termParser`)
-2- A tactic for proving the recursive applications are "decreasing" (`p` is `tacticSeq`)
+/--
+A decreasing_by clause can either be a single tactic (for all functions), or
+a list of tactics labeled with the function they apply to.
 -/
-def terminationHintMany (p : Parser) := leading_parser
-  atomic (lookahead (ident >> " => ")) >>
-  many1Indent (group (ppLine >> ppIndent (ident >> " => " >> p >> patternIgnore (optional ";"))))
-def terminationHint1 (p : Parser) := leading_parser p
-def terminationHint (p : Parser) := terminationHintMany p <|> terminationHint1 p
+def decreasingByElement := leading_parser
+  ppLine >> ppIndent (ident >> " => " >> Tactic.tacticSeq >> patternIgnore (optional ";"))
+def decreasingByMany := leading_parser
+  atomic (lookahead (ident >> " => ")) >> many1Indent decreasingByElement
+def decreasingBy1  := leading_parser Tactic.tacticSeq
 
-def terminationByCore := leading_parser
-  ppDedent ppLine >> "termination_by' " >> terminationHint termParser
 def decreasingBy := leading_parser
-  ppDedent ppLine >> "decreasing_by " >> terminationHint Tactic.tacticSeq
+  ppDedent ppLine >> "decreasing_by " >> (decreasingByMany <|> decreasingBy1)
 
 def terminationByElement   := leading_parser
   ppLine >> (ident <|> Term.hole) >> many (ppSpace >> (ident <|> Term.hole)) >>
@@ -53,7 +48,7 @@ def terminationBy          := leading_parser
   ppDedent ppLine >> "termination_by" >> many1Indent terminationByElement
 
 def terminationSuffix :=
-  optional (terminationBy <|> terminationByCore) >> optional decreasingBy
+  optional terminationBy >> optional decreasingBy
 
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 0699845ba4..658ab0874e 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -8,7 +8,7 @@ options get_default_options() {
     // switch to `true` for ABI-breaking changes affecting meta code
     opts = opts.update({"interpreter", "prefer_native"}, false);
     // switch to `true` for changing built-in parsers used in quotations
-    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false);
+    opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true);
     // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax
     // with custom precheck hooks were affected
     opts = opts.update({"quotPrecheck"}, true);
diff --git a/tests/lean/906.lean b/tests/lean/906.lean
index f92ab10552..4d8b56670a 100644
--- a/tests/lean/906.lean
+++ b/tests/lean/906.lean
@@ -3,7 +3,7 @@ def natPrintAux (n : Nat) (sink : List Char) : List Char :=
   if h0 : n < 10
   then (n.digitChar :: sink)
   else natPrintAux (n / 10) (Nat.digitChar (n % 10) :: sink)
-termination_by' measure (fun ⟨n, _⟩ => n)
+termination_by _ n => n
 decreasing_by sorry
 
 set_option maxRecDepth 100  -- default takes ages in debug mode and triggers stack space threshold
diff --git a/tests/lean/letRecMissingAnnotation.lean b/tests/lean/letRecMissingAnnotation.lean
index f9e466efe2..8cebbfa388 100644
--- a/tests/lean/letRecMissingAnnotation.lean
+++ b/tests/lean/letRecMissingAnnotation.lean
@@ -5,4 +5,4 @@ def sum (as : Array Nat) : Nat :=
     else
       s
   go 0 0
-termination_by' measure (fun ⟨i, _⟩ => as.size - i)
+termination_by go i _ => as.size - i
diff --git a/tests/lean/mutwf1.lean b/tests/lean/mutwf1.lean
index 16488d6658..82b74ff718 100644
--- a/tests/lean/mutwf1.lean
+++ b/tests/lean/mutwf1.lean
@@ -11,13 +11,9 @@ mutual
     else
       n
 end
-termination_by'
-  invImage
-    (fun
-     | PSum.inl ⟨n, true⟩ => (n, 2)
-     | PSum.inl ⟨n, false⟩ => (n, 1)
-     | PSum.inr n => (n, 0))
-  $ Prod.lex sizeOfWFRel sizeOfWFRel
+termination_by
+  f n b => (n, if b then 2 else 1)
+  g n => (n, 0)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index b887ea8a05..066ec9cf1a 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/tests/lean/mutwf1.lean.expected.out
@@ -1,9 +1,9 @@
-mutwf1.lean:28:2-28:6: error: unsolved goals
+mutwf1.lean:24:2-24:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0
 ⊢ Nat.sub n 0 ≠ 0
-mutwf1.lean:37:22-37:29: error: failed to prove termination, possible solutions:
+mutwf1.lean:33:22-33:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
   - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
diff --git a/tests/lean/run/860.lean b/tests/lean/run/860.lean
index 07377b7a55..106c708b39 100644
--- a/tests/lean/run/860.lean
+++ b/tests/lean/run/860.lean
@@ -21,8 +21,7 @@ def pack (n: Nat) : List Nat :=
       | true => loop (next n) 0 (List.cons acc accs)
       | false => loop (next n) (acc+1) accs
   loop n 0 []
-termination_by'
-  invImage (fun ⟨n, _, _⟩ => n) Nat.lt_wfRel
+termination_by _ n _ _ => n
 decreasing_by
   simp [invImage, InvImage, Prod.lex, sizeOfWFRel, measure, Nat.lt_wfRel]
   apply pack_loop_terminates
diff --git a/tests/lean/run/955.lean b/tests/lean/run/955.lean
index 07d5711a9c..16016899c8 100644
--- a/tests/lean/run/955.lean
+++ b/tests/lean/run/955.lean
@@ -11,16 +11,3 @@ termination_by _ n =>
   match n with
   | _ => n
 end Ex2
-
-
-namespace Ex3
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by' measure (fun n => match n with | PSum.inl n => n | PSum.inr n => n)
-end Ex3
diff --git a/tests/lean/run/eqnsAtSimp.lean b/tests/lean/run/eqnsAtSimp.lean
index a296c5f0f7..8a9e97a3dc 100644
--- a/tests/lean/run/eqnsAtSimp.lean
+++ b/tests/lean/run/eqnsAtSimp.lean
@@ -6,9 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by
   simp [measure, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.lt_succ_self
diff --git a/tests/lean/run/eqnsAtSimp2.lean b/tests/lean/run/eqnsAtSimp2.lean
index 8d7424a2af..646f12d499 100644
--- a/tests/lean/run/eqnsAtSimp2.lean
+++ b/tests/lean/run/eqnsAtSimp2.lean
@@ -6,9 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
@@ -20,7 +17,6 @@ def f (x : Nat) : Nat :=
   match x with
   | 0 => 1
   | x + 1 => f x * 2
-termination_by' measure id
 decreasing_by apply Nat.lt_succ_self
 
 attribute [simp] f
diff --git a/tests/lean/run/mutwf1.lean b/tests/lean/run/mutwf1.lean
index 6a6f9e9cb7..2e75be80be 100644
--- a/tests/lean/run/mutwf1.lean
+++ b/tests/lean/run/mutwf1.lean
@@ -12,35 +12,6 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
-
-#print f
-#print g
-#print h
-
-#eval f 5 'a' 'b'
-end Ex1
-
-namespace Ex2
-mutual
-  def f : Nat → α → α → α
-    | 0, a, b => a
-    | n, a, b => g a n b |>.1
-
-  def g : α → Nat → α → (α × α)
-    | a, 0, b => (a, b)
-    | a, n, b => (h a b n, a)
-
-  def h : α → α → Nat → α
-    | a, b, 0 => b
-    | a, b, n+1 => f n a b
-end
 termination_by
   f n _ _ => (n, 2)
   g _ n _ => (n, 1)
@@ -51,4 +22,4 @@ termination_by
 #print h
 
 #eval f 5 'a' 'b'
-end Ex2
+end Ex1
diff --git a/tests/lean/run/mutwf2.lean b/tests/lean/run/mutwf2.lean
index fa1d464595..d0cf4a6555 100644
--- a/tests/lean/run/mutwf2.lean
+++ b/tests/lean/run/mutwf2.lean
@@ -7,24 +7,9 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
+termination_by _ n => n
 
 #print isEven
 #print isOdd
 #print isEven._mutual
 end Ex1
-
-
-namespace Ex2
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by _ n => n
-end Ex2
diff --git a/tests/lean/run/mutwf3.lean b/tests/lean/run/mutwf3.lean
index 05af6cdd4f..596d1cf517 100644
--- a/tests/lean/run/mutwf3.lean
+++ b/tests/lean/run/mutwf3.lean
@@ -9,16 +9,13 @@ mutual
     | a, n, b => (h a b n, a)
 
   def h : α → α → Nat → α
-    | a, b, 0 => b
+    | _a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 decreasing_by
   simp_wf
   first
@@ -48,14 +45,30 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 
 #print f._unary._mutual
 
 end Ex2
+
+namespace Ex3
+mutual
+  def f : Nat → α → α → α
+    | 0, a, b => a
+    | n, a, b => g a n b |>.1
+
+  def g : α → Nat → α → (α × α)
+    | a, 0, b => (a, b)
+    | a, n, b => (h a b n, a)
+
+  def h : α → α → Nat → α
+    | a, b, 0 => b
+    | a, b, n+1 => f n a b
+end
+
+#print f._unary._mutual
+
+end Ex3
diff --git a/tests/lean/run/nestedIssueMatch.lean b/tests/lean/run/nestedIssueMatch.lean
index 8e945d8098..0e91aaf6ee 100644
--- a/tests/lean/run/nestedIssueMatch.lean
+++ b/tests/lean/run/nestedIssueMatch.lean
@@ -5,7 +5,6 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-termination_by' sorry
 decreasing_by sorry
 
 attribute [simp] g
diff --git a/tests/lean/run/nestedWF.lean b/tests/lean/run/nestedWF.lean
index d0afa39339..c69d755153 100644
--- a/tests/lean/run/nestedWF.lean
+++ b/tests/lean/run/nestedWF.lean
@@ -43,7 +43,6 @@ def g (t : Nat) : Nat := match t with
       | 0 => 0
       | m + 1 => g n
   | 0 => 0
-termination_by' sorry
 decreasing_by sorry
 
 theorem ex1 : g 0 = 0 := by
diff --git a/tests/lean/run/robinson.lean b/tests/lean/run/robinson.lean
index 97230e854f..8ccc15fb45 100644
--- a/tests/lean/run/robinson.lean
+++ b/tests/lean/run/robinson.lean
@@ -18,7 +18,7 @@ abbrev P (c : Option Subst) u v := match c with
   | none => strangers u v
   | some f => act f u = act f v
 
-def rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)
+instance rel : WellFoundedRelation (Term × Term) := measure (λ (u, v) => depth u + depth v)
 
 theorem decr_left (l₁ r₁ l₂ r₂ : Term) :
   rel.rel (l₁, l₂) (Term.Cons l₁ r₁, Term.Cons l₂ r₂) := by
@@ -41,7 +41,7 @@ def robinson (u v : Term) : { f : Option Subst // P f u v } := match u, v with
   | .Var i, .Var j =>
     if i = j then ⟨ some id, sorry ⟩
     else ⟨ some λ n => if n = i then j else n, sorry ⟩
-termination_by' invImage (λ ⟨ u, v ⟩ => (u, v)) rel
+termination_by _ u v => (u, v)
 decreasing_by
   first
     | apply decr_left _ _ _ _
diff --git a/tests/lean/run/wfEqns1.lean b/tests/lean/run/wfEqns1.lean
index 59c7de89b5..8daaab858e 100644
--- a/tests/lean/run/wfEqns1.lean
+++ b/tests/lean/run/wfEqns1.lean
@@ -13,9 +13,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun
-  | PSum.inl n => n
-  | PSum.inr n => n
 decreasing_by
   simp [measure, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.lt_succ_self
diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean
index 80228ba917..8d8ead2069 100644
--- a/tests/lean/run/wfEqns2.lean
+++ b/tests/lean/run/wfEqns2.lean
@@ -16,12 +16,9 @@ def h (i j : Nat) : Nat :=
   | 0 => g i 0
   | Nat.succ j => g i j
 end
-termination_by'
- invImage
-    (fun
-      | PSum.inl n => (n, 0)
-      | PSum.inr n => (n, 1))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  g i j => (i + j, 0)
+  h i j => (i + j, 1)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean
index d7c8c36943..850766036e 100644
--- a/tests/lean/run/wfEqns3.lean
+++ b/tests/lean/run/wfEqns3.lean
@@ -10,7 +10,6 @@ def f (x : Nat) : Nat :=
     1
   else
    f (x - 1) * 2
-termination_by' measure id
 decreasing_by
   apply Nat.pred_lt
   exact h
diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean
index 2e42ca81cf..865f0ed7e2 100644
--- a/tests/lean/run/wfEqns4.lean
+++ b/tests/lean/run/wfEqns4.lean
@@ -18,13 +18,10 @@ mutual
     | a, b, 0 => b
     | a, b, n+1 => f n a b
 end
-termination_by'
-  invImage
-    (fun
-      | PSum.inl ⟨n, _, _⟩ => (n, 2)
-      | PSum.inr <| PSum.inl ⟨_, n, _⟩ => (n, 1)
-      | PSum.inr <| PSum.inr ⟨_, _, n⟩ => (n, 0))
-    (Prod.lex sizeOfWFRel sizeOfWFRel)
+termination_by
+  f n _ _ => (n, 2)
+  g _ n _ => (n, 1)
+  h _ _ n => (n, 0)
 decreasing_by
   simp_wf
   first
diff --git a/tests/lean/run/wfSum.lean b/tests/lean/run/wfSum.lean
index e825eae564..764195fb12 100644
--- a/tests/lean/run/wfSum.lean
+++ b/tests/lean/run/wfSum.lean
@@ -6,4 +6,4 @@ where
       go (i+1) (s + as.get ⟨i, h⟩)
     else
       s
-termination_by' measure (fun ⟨i, s⟩ => as.size - i)
+termination_by _ i s => as.size - i
diff --git a/tests/lean/run/wfrecUnary.lean b/tests/lean/run/wfrecUnary.lean
index a6c49a9bbe..5f7e403db1 100644
--- a/tests/lean/run/wfrecUnary.lean
+++ b/tests/lean/run/wfrecUnary.lean
@@ -3,7 +3,6 @@ def f (n : Nat) : Nat :=
     1
   else
     2 * f (n-1)
-termination_by' measure id
 decreasing_by
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel]
   apply Nat.pred_lt h
diff --git a/tests/lean/substBadMotive.lean b/tests/lean/substBadMotive.lean
index d3621cdc2f..11c69899dc 100644
--- a/tests/lean/substBadMotive.lean
+++ b/tests/lean/substBadMotive.lean
@@ -13,7 +13,7 @@ namespace Ex3
 def heapifyDown (a : Array α) (i : Fin a.size) : Array α :=
   have : i < i := sorry
   heapifyDown a ⟨i.1, a.size_swap i i ▸ i.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
-termination_by' measure fun i => i.1
+termination_by _ i => i.1
 decreasing_by assumption
 end Ex3
 
@@ -34,6 +34,6 @@ def heapifyDown (lt : α → α → Bool) (a : Array α) (i : Fin a.size) : Arra
     heapifyDown lt a' ⟨j.1.1, a.size_swap i j ▸ j.1.2⟩ -- Error, failed to compute motive, `subst` is not applicable here
   else
     a
-termination_by' measure fun ⟨a, i⟩ => a.size - i.1
+termination_by _ a i => a.size - i.1
 decreasing_by assumption
 end Ex4
diff --git a/tests/lean/termination_by.lean b/tests/lean/termination_by.lean
index b1c239a99c..7e5ec0adca 100644
--- a/tests/lean/termination_by.lean
+++ b/tests/lean/termination_by.lean
@@ -5,20 +5,84 @@ mutual
   inductive Odd : Nat → Prop
     | step : Even n → Odd (n+1)
 end
-termination_by' measure
+termination_by _ n => n -- Error
 
 mutual
  def f (n : Nat) :=
    if n == 0 then 0 else f (n / 2) + 1
- termination_by' measure
+ termination_by _ => n -- Error
 end
 
+mutual
+ def f (n : Nat) :=
+   if n == 0 then 0 else f (n / 2) + 1
+end
+termination_by n => n -- Error
+
+
 def g' (n : Nat) :=
   match n with
   | 0 => 1
   | n+1 => g' n * 3
-termination_by'
-  h => measure
+termination_by
+  h' n => n -- Error
+
+def g' (n : Nat) :=
+  match n with
+  | 0 => 1
+  | n+1 => g' n * 3
+termination_by
+  g' n => n
+  _ n => n -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   isOd x => x -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   isEven y => y -- Error
+
+mutual
+  def isEven : Nat → Bool
+    | 0 => true
+    | n+1 => isOdd n
+  def isOdd : Nat → Bool
+    | 0 => false
+    | n+1 => isEven n
+end
+termination_by
+   isEven x => x
+   _ x => x
+   _ x => x + 1 -- Error
+
 
 namespace Test
 mutual
@@ -34,8 +98,8 @@ mutual
     | 0, a, b => b
     | n+1, a, b => f n a b
 end
-termination_by'
-  f => measure
-  g => measure
+termination_by
+  f n => n -- Error
+  g n => n
 
 end Test
diff --git a/tests/lean/termination_by.lean.expected.out b/tests/lean/termination_by.lean.expected.out
index 7e2cf1eb58..6374b804ce 100644
--- a/tests/lean/termination_by.lean.expected.out
+++ b/tests/lean/termination_by.lean.expected.out
@@ -1,4 +1,10 @@
 termination_by.lean:8:0-8:23: error: invalid 'termination_by' in mutually inductive datatype declaration
-termination_by.lean:13:1-13:24: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by.lean:21:2-21:3: error: function 'h' not found in current declaration
-termination_by.lean:39:2-39:14: error: invalid termination hint element, 'Test.g' and 'Test.f' are in the same clique
+termination_by.lean:13:1-13:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
+termination_by.lean:20:15-20:21: error: function 'n' not found in current declaration
+termination_by.lean:28:2-28:11: error: function 'h'' not found in current declaration
+termination_by.lean:36:2-36:10: error: invalid `termination_by` syntax, unnecessary else-case
+termination_by.lean:47:3-47:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
+termination_by.lean:59:3-59:14: error: function 'isOd' not found in current declaration
+termination_by.lean:71:3-71:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
+termination_by.lean:84:3-84:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
+termination_by.lean:102:2-102:10: error: invalid `termination_by` syntax, missing case for function 'Test.h'
diff --git a/tests/lean/termination_by2.lean b/tests/lean/termination_by2.lean
deleted file mode 100644
index e26fbd71e7..0000000000
--- a/tests/lean/termination_by2.lean
+++ /dev/null
@@ -1,68 +0,0 @@
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
- termination_by _ => n
-end
-
-mutual
- def f (n : Nat) :=
-   if n == 0 then 0 else f (n / 2) + 1
-end
-termination_by n => n
-
-
-def g' (n : Nat) :=
-  match n with
-  | 0 => 1
-  | n+1 => g' n * 3
-termination_by
-  g' n => n
-  _ n => n
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isOd x => x -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   isEven y => y -- Error
-
-mutual
-  def isEven : Nat → Bool
-    | 0 => true
-    | n+1 => isOdd n
-  def isOdd : Nat → Bool
-    | 0 => false
-    | n+1 => isEven n
-end
-termination_by
-   isEven x => x
-   _ x => x
-   _ x => x + 1 -- Error
diff --git a/tests/lean/termination_by2.lean.expected.out b/tests/lean/termination_by2.lean.expected.out
deleted file mode 100644
index 32628cf565..0000000000
--- a/tests/lean/termination_by2.lean.expected.out
+++ /dev/null
@@ -1,7 +0,0 @@
-termination_by2.lean:4:1-4:22: error: invalid 'termination_by' in 'mutual' block, it must be used after the 'end' keyword
-termination_by2.lean:11:15-11:21: error: function 'n' not found in current declaration
-termination_by2.lean:20:2-20:10: error: invalid `termination_by` syntax, unnecessary else-case
-termination_by2.lean:31:3-31:16: error: invalid `termination_by` syntax, missing case for function 'isOdd'
-termination_by2.lean:43:3-43:14: error: function 'isOd' not found in current declaration
-termination_by2.lean:55:3-55:16: error: invalid `termination_by` syntax, `isEven` case has already been provided
-termination_by2.lean:68:3-68:15: error: invalid `termination_by` syntax, the else-case (i.e., `_ ... => ...`) has already been specified
diff --git a/tests/lean/unfold1.lean b/tests/lean/unfold1.lean
index 6a77120289..d153f3c6f0 100644
--- a/tests/lean/unfold1.lean
+++ b/tests/lean/unfold1.lean
@@ -6,7 +6,6 @@ mutual
     | 0 => false
     | n+1 => isEven n
 end
-termination_by' measure fun | PSum.inl n => n | PSum.inr n => n
 decreasing_by apply Nat.lt_succ_self
 
 theorem isEven_double (x : Nat) : isEven (2 * x) = true := by
diff --git a/tests/lean/wf2.lean b/tests/lean/wf2.lean
index 94bc3a2907..fee98b464d 100644
--- a/tests/lean/wf2.lean
+++ b/tests/lean/wf2.lean
@@ -3,4 +3,4 @@ def g (x : Nat) (y : Nat) : Nat :=
     2 * g (x-1) y -- Error here
   else
     0
-termination_by' measure (·.1)
+termination_by g x y => x
diff --git a/tests/lean/wfrecUnusedLet.lean b/tests/lean/wfrecUnusedLet.lean
index 2a9f9dd07a..0108141e46 100644
--- a/tests/lean/wfrecUnusedLet.lean
+++ b/tests/lean/wfrecUnusedLet.lean
@@ -4,7 +4,6 @@ def f (n : Nat) : Nat :=
   else
     let y := 42
     2 * f (n-1)
-termination_by' measure id
 decreasing_by
   simp [measure, id, invImage, InvImage, Nat.lt_wfRel, WellFoundedRelation.rel]
   apply Nat.pred_lt h
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index 38c47c9012..40e1995eaf 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -3,4 +3,4 @@ WellFounded.fix f.proof_1 fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
-    2 * a (n - 1) (_ : (measure id).1 (n - 1) n)
+    2 * a (n - 1) (_ : (invImage (fun a => sizeOf a) instWellFoundedRelation).1 (n - 1) n)