diff -r 631ea563c20a -r 756f30eac792 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Wed May 16 19:15:45 2012 +0200
@@ -37,7 +37,7 @@
     by (induct arbitrary: ys, simp, clarsimp simp add: list_all2_Cons1, fast)
 qed
 
-lemma list_reflp:
+lemma list_reflp[reflp_preserve]:
   assumes "reflp R"
   shows "reflp (list_all2 R)"
 proof (rule reflpI)