diff -r dcdfb6355a05 -r 4de9ff3ea29a src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Sun Sep 13 22:25:21 2015 +0200
+++ b/src/HOL/HOLCF/ConvexPD.thy	Sun Sep 13 22:56:52 2015 +0200
@@ -414,14 +414,14 @@
 by (simp add: convex_map_def convex_bind_bind)
 
 lemma ep_pair_convex_map: "ep_pair e p \<Longrightarrow> ep_pair (convex_map\<cdot>e) (convex_map\<cdot>p)"
-apply default
+apply standard
 apply (induct_tac x rule: convex_pd_induct, simp_all add: ep_pair.e_inverse)
 apply (induct_tac y rule: convex_pd_induct)
 apply (simp_all add: ep_pair.e_p_below monofun_cfun)
 done
 
 lemma deflation_convex_map: "deflation d \<Longrightarrow> deflation (convex_map\<cdot>d)"
-apply default
+apply standard
 apply (induct_tac x rule: convex_pd_induct, simp_all add: deflation.idem)
 apply (induct_tac x rule: convex_pd_induct)
 apply (simp_all add: deflation.below monofun_cfun)