src/HOL/Library/FuncSet.thy

 lemma card_bij:
      "[|f \<in> A\<rightarrow>B; inj_on f A;
         g \<in> B\<rightarrow>A; inj_on g B; finite A; finite B|] ==> card(A) = card(B)"
   by (blast intro: card_inj order_antisym)
 
-
-(*The following declarations generate polymorphic Skolem functions for 
-  these theorems. Eventually they should become redundant, once this 
-  is done automatically.*)
-
-declare FuncSet.Pi_I [skolem]
-declare FuncSet.Pi_mono [skolem]
-declare FuncSet.extensionalityI [skolem]
-declare FuncSet.funcsetI [skolem]
-declare FuncSet.restrictI [skolem]
-declare FuncSet.restrict_in_funcset [skolem]
-
 end