# HG changeset patch
# User nipkow
# Date 967474939 -7200
# Node ID 71364b4872323a63fa0c0de352128d9525e2a661
# Parent  14dc0f8129016cd21d8931743eecfe3bde3d42b8
Removed map_compose from simpset.

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