diff -r b5058ba95e32 -r 00c436488398 src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Tue Feb 20 22:04:04 2018 +0100
+++ b/src/HOL/HOLCF/ConvexPD.thy	Tue Feb 20 22:25:23 2018 +0100
@@ -430,8 +430,8 @@
   assumes "finite_deflation d" shows "finite_deflation (convex_map\<cdot>d)"
 proof (rule finite_deflation_intro)
   interpret d: finite_deflation d by fact
-  have "deflation d" by fact
-  thus "deflation (convex_map\<cdot>d)" by (rule deflation_convex_map)
+  from d.deflation_axioms show "deflation (convex_map\<cdot>d)"
+    by (rule deflation_convex_map)
   have "finite (range (\<lambda>x. d\<cdot>x))" by (rule d.finite_range)
   hence "finite (Rep_compact_basis -` range (\<lambda>x. d\<cdot>x))"
     by (rule finite_vimageI, simp add: inj_on_def Rep_compact_basis_inject)