# HG changeset patch
# User urbanc
# Date 1141205319 -3600
# Node ID 7dc4fc25de8dd9275e2a74465f90fc6c0e87012c
# Parent  0eccb98b1fdbae1ca1c2846d00bd7231ccdd11ca
added fresh_fun_eqvt theorem to the theorem collection

diff -r 0eccb98b1fdb -r 7dc4fc25de8d src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 01 10:27:48 2006 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Mar 01 10:28:39 2006 +0100
@@ -670,6 +670,7 @@
        val fresh_bij         = thm "nominal.pt_fresh_bij";
        val pt_pi_rev         = thm "nominal.pt_pi_rev";
        val pt_rev_pi         = thm "nominal.pt_rev_pi";
+       val fresh_fun_eqvt    = thm "nominal.fresh_fun_equiv";
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
@@ -776,6 +777,7 @@
 	      let val thms1 = inst_pt_at [fresh_bij]
 		  and thms2 = inst_pt_pt_at_cp [fresh_bij_ineq]
 	      in [(("fresh_eqvt", thms1 @ thms2),[])] end
+            ||>> PureThy.add_thmss [(("fresh_fun_eqvt",inst_pt_at [fresh_fun_eqvt]),[])]
 	   end;
 
     in NominalData.put (fold Symtab.update (map (rpair ()) full_ak_names)