--- a/QuotList.thy	Fri Dec 04 16:40:23 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 16:53:11 2009 +0100
@@ -52,7 +52,7 @@
   apply(induct_tac a)
   apply(simp)
   apply(simp)
-  apply(simp add: Quotient_REP_reflp[OF q])
+  apply(simp add: Quotient_rep_reflp[OF q])
   apply(rule allI)+
   apply(rule list_rel_rel[OF q])
   done
@@ -114,11 +114,11 @@
 
 (* TODO: Rest are unused *)
 
-lemma LIST_map_id:
+lemma list_map_id:
   shows "map (\<lambda>x. x) = (\<lambda>x. x)"
   by simp
 
-lemma list_rel_EQ:
+lemma list_rel_eq:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
@@ -127,10 +127,9 @@
 apply(simp_all)
 done
 
-lemma list_rel_REFL:
+lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"
 by (induct x) (auto simp add: a)
 
-
 end