--- 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 **)