--- 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);