# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1389627730 0
# Node ID 040519ec99e95adb1d2ded1e9190e5131e3354e8
# Parent  35bb5b013f0e8585cd1f231544c978755259fe67
fixed bug with support and freshness lemmas not being simplified properly

diff -r 35bb5b013f0e -r 040519ec99e9 Nominal/Ex/TypeVarsTest.thy
--- a/Nominal/Ex/TypeVarsTest.thy	Sat Jan 11 23:17:23 2014 +0000
+++ b/Nominal/Ex/TypeVarsTest.thy	Mon Jan 13 15:42:10 2014 +0000
@@ -27,6 +27,7 @@
 term Foo
 term Bar
 
+thm lam.supp lam.fresh
 thm lam.distinct
 thm lam.induct
 thm lam.exhaust 
@@ -43,6 +44,7 @@
   PsiNil
 | Output "'alpha" "'alpha" "('alpha, 'beta, 'gamma) psi" 
 
+thm psi.supp psi.fresh
 
 nominal_datatype 'a foo = 
   Node x::"name" f::"'a foo" binds x in f
diff -r 35bb5b013f0e -r 040519ec99e9 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Jan 11 23:17:23 2014 +0000
+++ b/Nominal/Nominal2.thy	Mon Jan 13 15:42:10 2014 +0000
@@ -446,7 +446,9 @@
         addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
 
   (* filters the theorems that are of the form "qfv = supp" *)
-  fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ lhs $ _)) = member (op=) qfvs lhs
+  val qfv_names = map (fst o dest_Const) qfvs
+  fun is_qfv_thm (@{term Trueprop} $ (Const (@{const_name HOL.eq}, _) $ Const (lhs, _) $ _)) = 
+    member (op=) qfv_names lhs
   | is_qfv_thm _ = false
 
   val qsupp_constrs = qfv_defs