diff -r bce41bea3de2 -r 8287fb5b8d7a QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 16:01:23 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 16:12:40 2009 +0100
@@ -461,7 +461,7 @@
   REPEAT_ALL_NEW (FIRST' 
     [resolve_tac rel_eqvs,
      rtac @{thm IDENTITY_equivp},
-     rtac @{thm LIST_equivp}])
+     rtac @{thm list_equivp}])
 *}
 
 ML {*