src/HOLCF/Cprod.thy

--- a/src/HOLCF/Cprod.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Cprod.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -306,7 +306,7 @@
 done
 
 instance "*" :: (chfin, chfin) chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (erule compact_imp_max_in_chain)
 apply (rule_tac p="\<Squnion>i. Y i" in cprodE, simp)
 done