--- a/Nominal/Nominal2_Abs.thy	Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/Nominal2_Abs.thy	Wed Mar 27 16:08:30 2013 +0100
@@ -9,7 +9,7 @@
 section {* Abstractions *}
 
 fun
-  alpha_set 
+  alpha_set
 where
   alpha_set[simp del]:
   "alpha_set (bs, x) R f p (cs, y) \<longleftrightarrow> 
@@ -1079,18 +1079,11 @@
 lemma prod_fv_supp:
   shows "prod_fv supp supp = supp"
 by (rule ext)
-   (auto simp add: prod_fv.simps supp_Pair)
+   (auto simp add: supp_Pair)
 
 lemma prod_alpha_eq:
   shows "prod_alpha (op=) (op=) = (op=)"
   unfolding prod_alpha_def
   by (auto intro!: ext)
 
-
-
-
-
-
-
 end
-