--- a/src/HOL/Library/Fin_Fun.thy Mon Jun 08 08:38:53 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy Mon Jun 08 09:22:47 2009 +0200
@@ -1186,10 +1186,10 @@
proof -
from enum_distinct
have "card (set (enum :: char list)) = length (enum :: char list)"
- by -(rule distinct_card)
+ by - (rule distinct_card)
also have "set enum = (UNIV :: char set)" by auto
- also note enum_char
- finally show ?thesis by simp
+ also note enum_chars
+ finally show ?thesis by (simp add: chars_def)
qed
instantiation char :: card_UNIV begin