--- a/Nominal/Nominal2_FSet.thy	Wed Apr 07 23:39:08 2010 -0700
+++ b/Nominal/Nominal2_FSet.thy	Thu Apr 08 00:00:21 2010 -0700
@@ -24,23 +24,13 @@
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
 
-lemma permute_list_zero: "0 \<bullet> (x :: 'a list) = x"
-  by (rule permute_zero)
-
-lemma permute_fset_zero: "0 \<bullet> (x :: 'a fset) = x"
-  by (lifting permute_list_zero)
-
-lemma permute_list_plus: "(p + q) \<bullet> (x :: 'a list) = p \<bullet> q \<bullet> x"
-  by (rule permute_plus)
-
-lemma permute_fset_plus: "(p + q) \<bullet> (x :: 'a fset) = p \<bullet> q \<bullet> x"
-  by (lifting permute_list_plus)
-
-instance
-  apply default
-  apply (rule permute_fset_zero)
-  apply (rule permute_fset_plus)
-  done
+instance proof
+  fix x :: "'a fset" and p q :: "perm"
+  show "0 \<bullet> x = x"
+    by (lifting permute_zero [where 'a="'a list"])
+  show "(p + q) \<bullet> x = p \<bullet> q \<bullet> x"
+    by (lifting permute_plus [where 'a="'a list"])
+qed
 
 end