diff -r 8df5eabda5f6 -r 0ca392ab7f37 src/HOLCF/Discrete.thy
--- a/src/HOLCF/Discrete.thy	Wed Jan 16 22:41:49 2008 +0100
+++ b/src/HOLCF/Discrete.thy	Thu Jan 17 00:51:20 2008 +0100
@@ -61,7 +61,7 @@
 qed
 
 instance discr :: (type) chfin
-apply (intro_classes, clarify)
+apply intro_classes
 apply (rule_tac x=0 in exI)
 apply (unfold max_in_chain_def)
 apply (clarify, erule discr_chain0 [symmetric])