diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
--- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -422,7 +422,7 @@
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   proof (rule ext)+
@@ -576,7 +576,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   proof (rule ext)+
@@ -613,7 +613,7 @@
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
     divide plus minus unit_factor normalize
-    rewrites "dvd.dvd op * = Rings.dvd"
+    rewrites "dvd.dvd ( * ) = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   proof (rule ext)+