--- a/Quot/Nominal/Fv.thy	Mon Feb 22 12:12:32 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 13:41:13 2010 +0100
@@ -259,12 +259,15 @@
     let
       val ty = domain_type (fastype_of alpha);
       val var = Free("x", ty);
+      val var2 = Free("y", ty);
     in
-      alpha $ var $ var
-    end
-  val eqs = map build_alpha alphas
+      ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var)))
+    end;
+  val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas)
 in
-  @{term Trueprop} $ foldr1 HOLogic.mk_conj eqs
+  Logic.mk_conjunction
+  (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs,
+   @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs)
 end
 *}