diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/Deflation.thy
--- a/src/HOL/HOLCF/Deflation.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Deflation.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -161,7 +161,7 @@
 unfolding finite_deflation_def by simp
 
 lemma finite_deflation_bottom: "finite_deflation \<bottom>"
-by default simp_all
+by standard simp_all
 
 
 subsection {* Continuous embedding-projection pairs *}
@@ -358,7 +358,7 @@
 subsection {* Composing ep-pairs *}
 
 lemma ep_pair_ID_ID: "ep_pair ID ID"
-by default simp_all
+by standard simp_all
 
 lemma ep_pair_comp:
   assumes "ep_pair e1 p1" and "ep_pair e2 p2"