src/HOL/Library/Cardinality.thy

--- a/src/HOL/Library/Cardinality.thy	Mon Dec 09 11:17:34 2019 +0100
+++ b/src/HOL/Library/Cardinality.thy	Mon Dec 09 15:36:51 2019 +0000
@@ -161,7 +161,7 @@
 subclass finite
 proof
   from CARD_1 show "finite (UNIV :: 'a set)"
-    by (auto intro!: card_ge_0_finite)
+    using finite_UNIV_fun by fastforce
 qed
 
 end