--- a/Nominal/Abs.thy	Wed Mar 17 10:34:25 2010 +0100
+++ b/Nominal/Abs.thy	Wed Mar 17 11:53:56 2010 +0100
@@ -300,31 +300,38 @@
   apply(simp_all)
   done
 
-lemma supp_Abs_subset1:
-  fixes x::"'a::fs"
+lemma finite_supp_Abs_subset1:
+  assumes "finite (supp x)"
   shows "(supp x) - as \<subseteq> supp (Abs as x)"
   apply(simp add: supp_conv_fresh)
   apply(auto)
   apply(drule_tac supp_Abs_fun_fresh)
   apply(simp only: supp_Abs_fun_simp)
   apply(simp add: fresh_def)
-  apply(simp add: supp_finite_atom_set finite_supp)
+  apply(simp add: supp_finite_atom_set assms)
   done
 
-lemma supp_Abs_subset2:
-  fixes x::"'a::fs"
+lemma finite_supp_Abs_subset2:
+  assumes "finite (supp x)"
   shows "supp (Abs as x) \<subseteq> (supp x) - as"
   apply(rule supp_is_subset)
   apply(rule Abs_supports)
-  apply(simp add: finite_supp)
+  apply(simp add: assms)
+  done
+
+lemma finite_supp_Abs:
+  assumes "finite (supp x)"
+  shows "supp (Abs as x) = (supp x) - as"
+  apply(rule_tac subset_antisym)
+  apply(rule finite_supp_Abs_subset2[OF assms])
+  apply(rule finite_supp_Abs_subset1[OF assms])
   done
 
 lemma supp_Abs:
   fixes x::"'a::fs"
   shows "supp (Abs as x) = (supp x) - as"
-  apply(rule_tac subset_antisym)
-  apply(rule supp_Abs_subset2)
-  apply(rule supp_Abs_subset1)
+  apply(rule finite_supp_Abs)
+  apply(simp add: finite_supp)
   done
 
 instance abs :: (fs) fs