src/HOL/HOLCF/Library/Option_Cpo.thy

--- a/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/Library/Option_Cpo.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -269,7 +269,7 @@
 
 lemma deflation_option_map [domain_deflation]:
   "deflation d \<Longrightarrow> deflation (option_map d)"
-apply default
+apply standard
 apply (induct_tac x, simp_all add: deflation.idem)
 apply (induct_tac x, simp_all add: deflation.below)
 done