--- a/QuotMain.thy	Fri Dec 04 12:21:15 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 13:58:23 2009 +0100
@@ -146,7 +146,7 @@
 declare [[map "fun" = (fun_map, FUN_REL)]]
 
 lemmas [quotient_thm] = 
-  FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT
+  FUN_QUOTIENT LIST_QUOTIENT
 
 ML {* maps_lookup @{theory} "List.list" *}
 ML {* maps_lookup @{theory} "*" *}