diff -r 5ac9a74d22fd -r 2e174807c891 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Sep 27 09:51:15 2010 -0400
+++ b/Nominal/Nominal2.thy	Mon Sep 27 12:19:17 2010 -0400
@@ -571,12 +571,24 @@
   (* postprocessing of eq and fv theorems *)
 
   val qeq_iffs' = qeq_iffs
-    |> map (simplify (HOL_basic_ss addsimps 
-         (@{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]} @ qfv_supp_thms)))
+    |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+    |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
 
   val qsupp_constrs = qfv_defs
     |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
 
+  val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+  val transform_thms = 
+    [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, 
+      @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, 
+      @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, 
+      @{thm fresh_def[symmetric]}]
+
+  val qfresh_constrs = qsupp_constrs
+    |> map (fn thm => thm RS transform_thm) 
+    |> map (simplify (HOL_basic_ss addsimps transform_thms))
+
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -599,6 +611,7 @@
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
+     ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)