# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1283151129 -32400
# Node ID 2795499a20bdb02080c48c2e1da6e27b52810b1b
# Parent  27c7b620758cf0e972fba22428afd15cf09a2bed
Quotient Package: dont unfold mem_def, use rsp and prs instead

diff -r 27c7b620758c -r 2795499a20bd src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 15:44:33 2010 +0900
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Mon Aug 30 15:52:09 2010 +0900
@@ -619,10 +619,10 @@
 
 
 (* Since we use Ball and Bex during the lifting and descending,
-   we cannot deal with lemmas containing them, unless we unfold 
-   them by default. Also mem cannot be regularized in general. *)
+   we cannot deal with lemmas containing them, unless we unfold
+   them by default. *)
 
-val default_unfolds = @{thms Ball_def Bex_def mem_def}
+val default_unfolds = @{thms Ball_def Bex_def}
 
 
 (** descending as tactic **)