--- a/src/HOL/Presburger.thy Fri Jul 04 20:07:08 2014 +0200
+++ b/src/HOL/Presburger.thy Fri Jul 04 20:18:47 2014 +0200
@@ -54,8 +54,8 @@
"(d::'a::{comm_ring,Rings.dvd}) dvd D \<Longrightarrow> \<forall>x k. (\<not>d dvd x + t) = (\<not>d dvd (x - k*D) + t)"
"\<forall>x k. F = F"
apply (auto elim!: dvdE simp add: algebra_simps)
-unfolding mult_assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
-unfolding dvd_def mult_commute [of d]
+unfolding mult.assoc [symmetric] distrib_right [symmetric] left_diff_distrib [symmetric]
+unfolding dvd_def mult.commute [of d]
by auto
subsection{* The A and B sets *}