# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1323826362 0
# Node ID 32abaea424bda7335f0557fc852b6a6a17298fd0
# Parent  b4b71c167e062728a6584fb8a59657868fbf75f3
generated the correct thm-list for showing that qfv are equal to support

diff -r b4b71c167e06 -r 32abaea424bd Nominal/Nominal2.thy
--- 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 =