--- 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