added some lemmas to the collection "abs_fresh"

the lemmas are of the form

finite (supp x) ==> (b # [a].x) = (b=a \/ b # x)

previously only lemmas of the form

(b # [a].x) = (b=a \/ b # x)

with the type-constraint that x is finitely supported
were included.

--- a/src/HOL/Nominal/nominal_atoms.ML	Mon Jan 09 13:29:08 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Mon Jan 09 15:55:15 2006 +0100
@@ -750,8 +750,9 @@
               in [(("perm_dj", thms1 @ thms2),[])] end
             ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at_fs [fresh_iff]
-		  and thms2 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
-	    in [(("abs_fresh", thms1 @ thms2),[])] end
+                  and thms2 = inst_pt_at [fresh_iff]
+		  and thms3 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
+	    in [(("abs_fresh", thms1 @ thms2 @ thms3),[])] end
 	    ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_supp]
 		  and thms2 = inst_pt_at_fs [abs_fun_supp]