compact_chfin is now declared simp

--- a/src/HOLCF/Up.thy	Mon Jan 14 03:56:31 2008 +0100
+++ b/src/HOLCF/Up.thy	Mon Jan 14 03:58:30 2008 +0100
@@ -344,8 +344,7 @@
 instance u :: (chfin) chfin
 apply (intro_classes, clarify)
 apply (erule compact_imp_max_in_chain)
-apply (rule_tac p="\<Squnion>i. Y i" in upE)
-apply (simp, simp add: compact_chfin)
+apply (rule_tac p="\<Squnion>i. Y i" in upE, simp_all)
 done
 
 text {* properties of fup *}