--- a/LFex.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/LFex.thy	Fri Dec 04 12:20:49 2009 +0100
@@ -219,7 +219,7 @@
 ML {*
   val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM}
   val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs}
-  val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}
+  val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot
   val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
   val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
 *}