src/HOL/List.ML

--- a/src/HOL/List.ML	Tue Aug 17 22:24:15 1999 +0200
+++ b/src/HOL/List.ML	Wed Aug 18 10:27:57 1999 +0200
@@ -770,6 +770,7 @@
 by (exhaust_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "take_all";
+Addsimps [take_all];
 
 Goal "!xs. length xs <= n --> drop n xs = []";
 by (induct_tac "n" 1);
@@ -777,6 +778,7 @@
 by (exhaust_tac "xs" 1);
  by Auto_tac;
 qed_spec_mp "drop_all";
+Addsimps [drop_all];
 
 Goal "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
 by (induct_tac "n" 1);