X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnDestructTac.ml;h=f03baa65645b5bf1e9ee33414fc0b47f89040319;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=fdee9e12713a103b5fea02848b3ce5ffb48d7745;hpb=3ca25660341410dd0f8694e6863c7c16f4e912a7;p=helm.git

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index fdee9e127..f03baa656 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -321,11 +321,11 @@ let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
   (* PHASE 2: create the object for the proof of the principle: we'll name it
    * "theorem" *)
   let status, theorem =
-   GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+   let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+   GrafiteDisambiguate.disambiguate_nobj status ~baseuri
     (baseuri ^ name ^ ".def",0,
       NotationPt.Theorem
-       (`Theorem,name,principle,
-         Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+       (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
   in 
   let uri,height,nmenv,nsubst,nobj = theorem in
   let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in