--- a/src/HOLCF/ConvexPD.thy Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/ConvexPD.thy Wed Jun 18 23:03:11 2008 +0200
@@ -236,12 +236,7 @@
lemma compact_imp_convex_principal:
"compact xs \<Longrightarrow> \<exists>t. xs = convex_principal t"
-apply (drule bifinite_compact_eq_approx)
-apply (erule exE)
-apply (erule subst)
-apply (cut_tac n=i and xs=xs in approx_eq_convex_principal)
-apply fast
-done
+by (rule convex_pd.compact_imp_principal)
lemma convex_principal_induct:
"\<lbrakk>adm P; \<And>t. P (convex_principal t)\<rbrakk> \<Longrightarrow> P xs"