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

diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma
index a0d3a0bd6..138e37e71 100644
--- a/helm/software/matita/tests/decl.ma
+++ b/helm/software/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