--- a/Quot/QuotList.thy	Fri Jan 08 10:08:01 2010 +0100
+++ b/Quot/QuotList.thy	Fri Jan 08 10:39:08 2010 +0100
@@ -183,9 +183,7 @@
 apply (simp_all)
 done
 
-(* Rest are unused *)
-
-lemma list_rel_eq:
+lemma list_rel_eq[id_simps]:
   shows "list_rel (op =) \<equiv> (op =)"
 apply(rule eq_reflection)
 unfolding expand_fun_eq
@@ -194,6 +192,8 @@
 apply(simp_all)
 done
 
+(* Rest are unused *)
+
 lemma list_rel_refl:
   assumes a: "\<And>x y. R x y = (R x = R y)"
   shows "list_rel R x x"