diff -r 8287fb5b8d7a -r c0b13fb70d6d QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:40:23 2009 +0100
@@ -1081,7 +1081,7 @@
     val thy = ProofContext.theory_of lthy;
     val quotients = quotient_rules_get lthy
     val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
-    val absrep = map (fn x => @{thm Quotient_ABS_REP} OF [x]) quotients
+    val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quotients
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same