diff -r add799cf0817 -r 82e37a4595c7 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Wed Nov 10 13:46:21 2010 +0000
+++ b/Nominal-General/Nominal2_Base.thy	Fri Nov 12 01:20:53 2010 +0000
@@ -142,6 +142,7 @@
   "Rep_perm p1 = Rep_perm p2 \<Longrightarrow> p1 = p2"
   by (simp add: fun_eq_iff Rep_perm_inject [symmetric])
 
+instance perm :: size ..
 
 subsection {* Permutations form a group *}