--- a/QuotList.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -16,6 +16,7 @@
 
 lemma LIST_REL_EQ:
   shows "LIST_REL (op =) \<equiv> (op =)"
+apply(rule eq_reflection)
 unfolding expand_fun_eq
 apply(rule allI)+
 apply(induct_tac x xa rule: list_induct2')