src/HOLCF/Discrete.thy

--- a/src/HOLCF/Discrete.thy	Fri Oct 22 07:44:34 2010 -0700
+++ b/src/HOLCF/Discrete.thy	Fri Oct 22 07:45:32 2010 -0700
@@ -44,13 +44,6 @@
  "!!S::nat=>('a::type)discr. chain(S) ==> range(S) = {S 0}"
 by (fast elim: discr_chain0)
 
-instance discr :: (type) chfin
-apply intro_classes
-apply (rule_tac x=0 in exI)
-apply (unfold max_in_chain_def)
-apply (clarify, erule discr_chain0 [symmetric])
-done
-
 subsection {* \emph{undiscr} *}
 
 definition