X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Ftests%2Fdecl.ma;h=138e37e71fbbd941ad9c48559796071d5d7d0135;hb=26bd030af58a7f4a5dff3c41ad5431e31e851d3e;hp=a0d3a0bd610f62962e0ffb73ea4d718985f49a21;hpb=9d5de2f3f3a8921397b939ce2143b22aa71959ea;p=helm.git

diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma
index a0d3a0bd6..138e37e71 100644
--- a/matita/tests/decl.ma
+++ b/matita/tests/decl.ma
@@ -200,7 +200,7 @@ theorem easy6: ∀t. O ≮ O → O < size t → t ≠ Empty.
      suppose (Node t1 t2 = Empty) (absurd).
      (* Discriminate should really generate a theorem to be useful with
         declarative tactics *)
-     discriminate absurd.
+     destruct absurd.
      by final
    done.
 qed.
\ No newline at end of file