X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fturing%2Fturing_old.ma;h=cafe3aadc6a7b1e6250541d3279cce33edcf86c2;hb=64a752136a679bcab14a9cd01823c18b7cc991de;hp=f50426985a0194ae2ba83ab819790fec91838181;hpb=65a3b93b01f2d00960c56df3563b879f36f3cbfd;p=helm.git

diff --git a/matita/matita/lib/turing/turing_old.ma b/matita/matita/lib/turing/turing_old.ma
index f50426985..cafe3aadc 100644
--- a/matita/matita/lib/turing/turing_old.ma
+++ b/matita/matita/lib/turing/turing_old.ma
@@ -49,7 +49,7 @@ normalize >(len A n v) //
 qed.
 
 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
-#A #B #l #f elim l // #a #tl #Hind normalize //
+#A #B #l #f elim l //
 qed.
 
 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.