diff -r d3f2038198ae -r a3cc9fa1295d src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Wed Mar 31 11:24:46 2021 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Wed Mar 31 18:18:03 2021 +0200
@@ -438,8 +438,9 @@
     by (rule interval_integral_endpoints_reverse)
   show ?thesis
     using integrable
-    by (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
-       (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
+    apply (cases a b b c a c rule: linorder_le_cases[case_product linorder_le_cases linorder_cases])
+    apply simp_all (* remove some looping cases *)
+    by (simp_all add: min_absorb1 min_absorb2 max_absorb1 max_absorb2 field_simps 1 2 3)
 qed
 
 lemma interval_integrable_isCont: