diff -r a2db1e379778 -r 5ebfb7f25ebb src/HOLCF/UpperPD.thy
--- a/src/HOLCF/UpperPD.thy	Wed Jun 18 22:32:06 2008 +0200
+++ b/src/HOLCF/UpperPD.thy	Wed Jun 18 23:03:11 2008 +0200
@@ -186,12 +186,7 @@
 
 lemma compact_imp_upper_principal:
   "compact xs \<Longrightarrow> \<exists>t. xs = upper_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_upper_principal)
-apply fast
-done
+by (rule upper_pd.compact_imp_principal)
 
 lemma upper_principal_induct:
   "\<lbrakk>adm P; \<And>t. P (upper_principal t)\<rbrakk> \<Longrightarrow> P xs"