diff -r 5bc338cee4a0 -r dd675800469d src/HOL/Computational_Algebra/Field_as_Ring.thy
--- a/src/HOL/Computational_Algebra/Field_as_Ring.thy	Wed Oct 09 23:00:52 2019 +0200
+++ b/src/HOL/Computational_Algebra/Field_as_Ring.thy	Wed Oct 09 14:51:54 2019 +0000
@@ -35,7 +35,7 @@
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end
 
@@ -66,7 +66,7 @@
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end
 
@@ -97,7 +97,7 @@
 
 instance
   by standard
-    (simp_all add: dvd_field_iff divide_simps split: if_splits)
+    (simp_all add: dvd_field_iff field_split_simps split: if_splits)
 
 end