diff -r 14dc0f812901 -r 71364b487232 src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Aug 28 16:53:35 2000 +0200
+++ b/src/HOL/List.ML	Mon Aug 28 17:02:19 2000 +0200
@@ -312,7 +312,7 @@
 by (induct_tac "xs" 1);
 by Auto_tac;
 qed "map_compose";
-Addsimps[map_compose];
+(*Addsimps[map_compose];*)
 
 Goal "rev(map f xs) = map f (rev xs)";
 by (induct_tac "xs" 1);