src/HOL/Rings.thy

--- a/src/HOL/Rings.thy	Wed May 11 10:42:24 2022 +0200
+++ b/src/HOL/Rings.thy	Tue May 17 14:10:14 2022 +0100
@@ -2408,7 +2408,7 @@
   proof (rule ccontr, simp add: not_less)
     assume "b \<le> a"
     with that show False
-      by (simp add: )
+      by simp
   qed
 qed