diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Analysis/Simplex_Content.thy
--- a/src/HOL/Analysis/Simplex_Content.thy	Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Analysis/Simplex_Content.thy	Wed Oct 09 14:51:54 2019 +0000
@@ -252,7 +252,7 @@
                     ((a + b + c) - 2 * c)"
     unfolding power2_eq_square by (simp add: s_def a_def b_def c_def algebra_simps)
   also have "\<dots> = 16 * s * (s - a) * (s - b) * (s - c)"
-    by (simp add: s_def divide_simps mult_ac)
+    by (simp add: s_def field_split_simps mult_ac)
   finally have "content (convex hull {A, B, C}) ^ 2 = s * (s - a) * (s - b) * (s - c)"
     by simp
   also have "\<dots> = sqrt (s * (s - a) * (s - b) * (s - c)) ^ 2"