diff -r e5fcbf6dc687 -r c17d0227205c src/HOL/MicroJava/Comp/CorrCompTp.thy
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy	Mon Aug 31 22:05:05 2020 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy	Tue Sep 01 16:57:54 2020 +0200
@@ -451,10 +451,7 @@
   "max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)" 
   apply (simp add: max_of_list_def)
   apply (induct xs)
-   apply simp
-  using [[linarith_split_limit = 0]]
-  apply simp
-  apply arith
+   apply simp_all
   done