# HG changeset patch
# User nipkow
# Date 932288768 -7200
# Node ID 6ea3b385e7317b0aab2d63ee66671f0de808800a
# Parent  ca0fbe679bbbd50a8cf82132d02299a7152522d0
Modifid length_tl

diff -r ca0fbe679bbb -r 6ea3b385e731 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jul 16 22:27:16 1999 +0200
+++ b/src/HOL/List.ML	Sun Jul 18 11:06:08 1999 +0200
@@ -87,7 +87,7 @@
 qed "length_rev";
 Addsimps [length_rev];
 
-Goal "xs ~= [] ==> length(tl xs) = (length xs) - 1";
+Goal "length(tl xs) = (length xs) - 1";
 by (exhaust_tac "xs" 1);
 by Auto_tac;
 qed "length_tl";