From 80e2e1daa86f90ce1d0d55aaa2a1fc6a63883bf2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 11 Feb 2022 16:22:13 +0100
Subject: [PATCH] test: mutual block not needed

---
 tests/lean/run/letrecWFIssue.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tests/lean/run/letrecWFIssue.lean b/tests/lean/run/letrecWFIssue.lean
index ba260e3eb5..17158fcdca 100644
--- a/tests/lean/run/letrecWFIssue.lean
+++ b/tests/lean/run/letrecWFIssue.lean
@@ -8,7 +8,6 @@ inductive TreeList (α : Type u) where
   | cons : Tree α → TreeList α → TreeList α
 end
 
-mutual
 def Tree.size : Tree α → Nat
   | Tree.node l =>
     -- see "TODO: linarith" in Init.WFTactics
@@ -29,7 +28,6 @@ where sizeList : TreeList α → Nat
       apply Nat.lt_succ_of_le
       apply Nat.le_add_left
     t.size + sizeList l
-end
 -- use automatically synthesized size function, which is not quite the number of leaves
 termination_by
   size t => sizeOf t