diff -r 792691e4b311 -r 12a6088ed195 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Feb 15 08:17:46 2015 +0100
+++ b/src/HOL/GCD.thy	Sun Feb 15 17:01:22 2015 +0100
@@ -334,8 +334,7 @@
   + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
 apply default
 apply (auto intro: dvd_antisym dvd_trans)[4]
-apply (metis dvd.dual_order.refl gcd_unique_nat)
-apply (auto intro: dvdI elim: dvdE)
+apply (metis dvd.dual_order.refl gcd_unique_nat)+
 done
 
 interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"