--- a/LFex.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/LFex.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -219,9 +219,7 @@
 ML {*
   val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
   val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
-  (*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
+  val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
 *}
 
 lemma