diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -25,14 +25,14 @@
       and r_cancel: 
           "\<And>a b c. \<lbrakk>a \<otimes> c = b \<otimes> c; a \<in> carrier G; b \<in> carrier G; c \<in> carrier G\<rbrakk> \<Longrightarrow> a = b"
   shows "monoid_cancel G"
-    by default fact+
+    by standard fact+
 
 lemma (in monoid_cancel) is_monoid_cancel:
   "monoid_cancel G"
   ..
 
 sublocale group \<subseteq> monoid_cancel
-  by default simp_all
+  by standard simp_all
 
 
 locale comm_monoid_cancel = monoid_cancel + comm_monoid
@@ -3640,7 +3640,7 @@
 done
 
 sublocale factorial_monoid \<subseteq> primeness_condition_monoid
-  by default (rule irreducible_is_prime)
+  by standard (rule irreducible_is_prime)
 
 
 lemma (in factorial_monoid) primeness_condition:
@@ -3649,10 +3649,10 @@
 
 lemma (in factorial_monoid) gcd_condition [simp]:
   shows "gcd_condition_monoid G"
-  by default (rule gcdof_exists)
+  by standard (rule gcdof_exists)
 
 sublocale factorial_monoid \<subseteq> gcd_condition_monoid
-  by default (rule gcdof_exists)
+  by standard (rule gcdof_exists)
 
 lemma (in factorial_monoid) division_weak_lattice [simp]:
   shows "weak_lattice (division_rel G)"