diff -r 768c5d319a0a -r 50219e796e05 QuotMain.thy
--- a/QuotMain.thy	Sat Oct 17 12:31:48 2009 +0200
+++ b/QuotMain.thy	Sat Oct 17 12:44:58 2009 +0200
@@ -1237,7 +1237,11 @@
 prefer 3
 (* APPLY_RSP *)
 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]
-apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"])
+(* MINE *)
+prefer 4
+apply (rule list_eq_refl )
+
 sorry
 
 thm list.recs(2)