X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=8267fd87774e00398ea654d17ba0a6ff4111c1ae;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=12e14be46b0a9163c12716ddd859b6d12bf2d4a8;hpb=e4328c9691fa85434acfb24eaedcb15ea2263b28;p=helm.git

diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml
index 12e14be46..8267fd877 100644
--- a/matita/components/ng_tactics/nInversion.ml
+++ b/matita/components/ng_tactics/nInversion.ml
@@ -150,11 +150,11 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
         mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
      in
      let status, theorem =
-      GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+      let attrs = `Generated, `Theorem, `InversionPrinciple in 
+      GrafiteDisambiguate.disambiguate_nobj status ~baseuri
        (baseuri ^ name ^ ".def",0,
          NotationPt.Theorem
-          (`Theorem,name,theorem,
-            Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+          (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
      in 
      let uri,height,nmenv,nsubst,nobj = theorem in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in