--- a/Nominal/ExPS3.thy	Tue Mar 23 10:24:12 2010 +0100
+++ b/Nominal/ExPS3.thy	Tue Mar 23 10:26:46 2010 +0100
@@ -29,7 +29,8 @@
 thm exp_pat3.perm
 thm exp_pat3.induct
 thm exp_pat3.distinct
-thm exp_pat3.fv[simplified exp_pat3.supp]
+thm exp_pat3.fv
+thm exp_pat3.supp (* The bindings are too complicated *)
 
 end