--- a/Nominal/Nominal2.thy	Tue Dec 13 09:39:56 2011 +0000
+++ b/Nominal/Nominal2.thy	Wed Dec 14 01:32:42 2011 +0000
@@ -437,14 +437,19 @@
   val qfv_supp_thms = 
     prove_fv_supp qtys (flat qtrms) qfvs qfv_bns qalpha_bns qfv_defs qeq_iffs 
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
+    |> map Drule.eta_contraction_rule
 
   (* postprocessing of eq and fv theorems *)
   val qeq_iffs' = qeq_iffs
     |> 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]}))
 
+  (* filters the theormes that are of the form "qfv = supp" *)
+  fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs
+  | is_qfv_thm _ = false
+
   val qsupp_constrs = qfv_defs
-    |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+    |> map (simplify (HOL_basic_ss addsimps (filter (is_qfv_thm o prop_of) qfv_supp_thms)))
 
   val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
   val transform_thms =