--- a/src/HOL/Library/FuncSet.thy Tue Aug 08 18:40:20 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy Tue Aug 08 18:40:56 2006 +0200
@@ -219,4 +219,16 @@
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