src/HOL/Library/Cardinality.thy
changeset 67091 1393c2340eec
parent 62597 b3f2b8c906a6
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Cardinality.thy	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Library/Cardinality.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4        unfolding bs[symmetric] distinct_card[OF distb] ..
     1.5      have ca: "CARD('a) = length as"
     1.6        unfolding as[symmetric] distinct_card[OF dista] ..
     1.7 -    let ?xs = "map (\<lambda>ys. the o map_of (zip as ys)) (List.n_lists (length as) bs)"
     1.8 +    let ?xs = "map (\<lambda>ys. the \<circ> map_of (zip as ys)) (List.n_lists (length as) bs)"
     1.9      have "UNIV = set ?xs"
    1.10      proof(rule UNIV_eq_I)
    1.11        fix f :: "'a \<Rightarrow> 'b"