--- a/Nominal/Nominal2.thy	Mon Sep 27 04:56:49 2010 -0400
+++ b/Nominal/Nominal2.thy	Mon Sep 27 09:51:15 2010 -0400
@@ -568,7 +568,15 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
- 
+  (* 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)))
+
+  val qsupp_constrs = qfv_defs
+    |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -578,7 +586,7 @@
 
   val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
-     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
@@ -590,7 +598,7 @@
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
-     ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
+     ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)