diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -88,7 +88,7 @@
   "perms = {f. bij f \<and> finite {x. f x \<noteq> x}}"
 
 typedef 'a perm = "perms :: ('a \<Rightarrow> 'a) set"
-  by (default) (auto simp: perms_def)
+  by standard (auto simp: perms_def)
 
 text {*First we need some auxiliary lemmas.*}
 lemma permsI [Pure.intro]:
@@ -153,13 +153,14 @@
   unfolding uminus_perm_def by (simp add: Abs_perm_inverse perms_inv Rep_perm)
 
 instance
-  apply default
+  apply standard
   unfolding Rep_perm_inject [symmetric]
   unfolding minus_perm_def
   unfolding Rep_perm_add
   unfolding Rep_perm_uminus
   unfolding Rep_perm_0
-  by (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+  apply (simp_all add: o_assoc inv_o_cancel [OF bij_is_inj [OF bij_Rep_perm]])
+  done
 
 end
 
@@ -198,7 +199,7 @@
   PERMUTE permute_atom
 
 interpretation atom_permute: permute permute_atom
-  by (default) (simp add: permute_atom_def Rep_perm_simps)+
+  by standard (simp_all add: permute_atom_def Rep_perm_simps)
 
 text {*Permuting permutations.*}
 definition permute_perm :: "'a perm \<Rightarrow> 'a perm \<Rightarrow> 'a perm" where
@@ -208,7 +209,7 @@
   PERMUTE permute_perm
 
 interpretation perm_permute: permute permute_perm
-  apply default
+  apply standard
   unfolding permute_perm_def
   apply simp
   apply (simp only: diff_conv_add_uminus minus_add add.assoc)