Closed some daemons

[helm.git] / matita / matita / lib / turing / turing_old.ma

diff --git a/matita/matita/lib/turing/turing_old.ma b/matita/matita/lib/turing/turing_old.ma
index f50426985a0194ae2ba83ab819790fec91838181..cafe3aadc6a7b1e6250541d3279cce33edcf86c2 100644 (file)
--- 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.