diff -r 894599a50af3 -r cda25f9aa678 Attic/Quot/Examples/FSet_BallBex.thy
--- a/Attic/Quot/Examples/FSet_BallBex.thy	Sat Sep 04 07:39:38 2010 +0800
+++ b/Attic/Quot/Examples/FSet_BallBex.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -11,15 +11,13 @@
   apply (metis mem_def)
   done
 
-(* Should not work and doesn't.
 thm test[quot_lifted]
-*)
 
 lemma "\<forall>xs \<in> (\<lambda>xs. x |\<in>| xs). x |\<in>| finsert y xs"
-  unfolding Ball_def mem_def
-  by (lifting test[unfolded Ball_def mem_def])
+  unfolding Ball_def
+  by (lifting test[unfolded Ball_def])
 
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def mem_def} @{thm test}*}
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Ball_def Bex_def} @{thm test}*}
 
 lemma test2:
   "\<exists>xs \<in> (\<lambda>xs. xs \<approx> []). xs \<approx> []"
@@ -27,14 +25,12 @@
   apply (auto simp add: mem_def)
   done
 
-(* Should not work and doesn't
 thm test2[quot_lifted]
-*)
 
 lemma "\<exists>xs \<in> (\<lambda>xs. xs = {||}). xs = {||}"
-  unfolding Bex_def mem_def
-  by (lifting test2[unfolded Bex_def mem_def])
+  unfolding Bex_def
+  by (lifting test2[unfolded Bex_def])
 
-ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def mem_def} @{thm test2}*}
+ML {* Quotient_Tacs.lifted @{context} [@{typ "'a fset"}] @{thms Bex_def} @{thm test2}*}
 
 end