src/HOL/Library/Cardinality.thy
changeset 49948 744934b818c7
parent 49689 b8a710806de9
child 51116 0dac0158b8d4
--- a/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:09:37 2012 +0200
+++ b/src/HOL/Library/Cardinality.thy	Sat Oct 20 09:12:16 2012 +0200
@@ -92,7 +92,7 @@
       unfolding bs[symmetric] distinct_card[OF distb] ..
     have ca: "CARD('a) = length as"
       unfolding as[symmetric] distinct_card[OF dista] ..
-    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (Enum.n_lists (length as) bs)"
+    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)"
     have "UNIV = set ?xs"
     proof(rule UNIV_eq_I)
       fix f :: "'a \<Rightarrow> 'b"
@@ -103,8 +103,8 @@
     moreover have "distinct ?xs" unfolding distinct_map
     proof(intro conjI distinct_n_lists distb inj_onI)
       fix xs ys :: "'b list"
-      assume xs: "xs \<in> set (Enum.n_lists (length as) bs)"
-        and ys: "ys \<in> set (Enum.n_lists (length as) bs)"
+      assume xs: "xs \<in> set (List.n_lists (length as) bs)"
+        and ys: "ys \<in> set (List.n_lists (length as) bs)"
         and eq: "the \<circ> map_of (zip as xs) = the \<circ> map_of (zip as ys)"
       from xs ys have [simp]: "length xs = length as" "length ys = length as"
         by(simp_all add: length_n_lists_elem)
@@ -472,3 +472,4 @@
 hide_const (open) card' finite' subset' eq_set
 
 end
+