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