diff -r 631ea563c20a -r 756f30eac792 src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed May 16 18:16:51 2012 +0200
+++ b/src/HOL/Lifting.thy	Wed May 16 19:15:45 2012 +0200
@@ -100,6 +100,9 @@
 lemma identity_quotient: "Quotient (op =) id id (op =)"
 unfolding Quotient_def by simp 
 
+lemma reflp_equality: "reflp (op =)"
+by (auto intro: reflpI)
+
 text {* TODO: Use one of these alternatives as the real definition. *}
 
 lemma Quotient_alt_def:
@@ -364,6 +367,7 @@
 setup Lifting_Info.setup
 
 declare fun_quotient[quot_map]
+declare reflp_equality[reflp_preserve]
 
 use "Tools/Lifting/lifting_term.ML"