diff -r c0b13fb70d6d -r 94deffed619d QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -1062,7 +1062,7 @@
  - Rewriting with definitions from the argument defs
      NewConst  ---->  (rep ---> abs) oldConst
 
- - Quotient_REL_REP:
+ - Quotient_rel_rep:
      Rel (Rep x) (Rep y)  ---->  x = y
 
  - ABS_REP
@@ -1082,11 +1082,9 @@
     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 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
+    val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients
     val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
-      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
+      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs)
   in
     EVERY' [
       (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))  ---->  f *)