--- a/Quot/Nominal/Fv.thy	Mon Feb 22 13:41:13 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Mon Feb 22 14:50:53 2010 +0100
@@ -260,14 +260,19 @@
       val ty = domain_type (fastype_of alpha);
       val var = Free("x", ty);
       val var2 = Free("y", ty);
+      val var3 = Free("z", ty);
+      val symp = HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var);
+      val transp = HOLogic.mk_imp (alpha $ var $ var2,
+        HOLogic.mk_all ("z", ty,
+          HOLogic.mk_imp (alpha $ var2 $ var3, alpha $ var $ var3)))
     in
-      ((alpha $ var $ var), (HOLogic.mk_imp (alpha $ var $ var2, alpha $ var2 $ var)))
+      ((alpha $ var $ var), (symp, transp))
     end;
-  val (refl_eqs, sym_eqs) = split_list (map build_alpha alphas)
+  val (refl_eqs, eqs) = split_list (map build_alpha alphas)
+  val (sym_eqs, trans_eqs) = split_list eqs
+  fun conj l = @{term Trueprop} $ foldr1 HOLogic.mk_conj l
 in
-  Logic.mk_conjunction
-  (@{term Trueprop} $ foldr1 HOLogic.mk_conj refl_eqs,
-   @{term Trueprop} $ foldr1 HOLogic.mk_conj sym_eqs)
+  (conj refl_eqs, (conj sym_eqs, conj trans_eqs))
 end
 *}