X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationUtil.ml;h=3683c0c0e80383996751eb6c6858c31f552cd179;hb=06d5ff2316426acfb16a9cc9784d40ce19351771;hp=3d80e8fd51427a0d091335a95e186b1b4553d91f;hpb=d4f2d4c1a4784f84aa27e1bb96b8b377a6553c65;p=helm.git

diff --git a/matita/components/content/notationUtil.ml b/matita/components/content/notationUtil.ml
index 3d80e8fd5..3683c0c0e 100644
--- a/matita/components/content/notationUtil.ml
+++ b/matita/components/content/notationUtil.ml
@@ -386,11 +386,11 @@ let freshen_obj obj =
           indtypes
       in
       NotationPt.Inductive (freshen_capture_variables params, indtypes)
-  | NotationPt.Theorem (flav, n, t, ty_opt,p) ->
+  | NotationPt.Theorem (n, t, ty_opt, attrs) ->
       let ty_opt =
         match ty_opt with None -> None | Some ty -> Some (freshen_term ty)
       in
-      NotationPt.Theorem (flav, n, freshen_term t, ty_opt,p)
+      NotationPt.Theorem (n, freshen_term t, ty_opt, attrs)
   | NotationPt.Record (params, n, ty, fields) ->
       NotationPt.Record (freshen_capture_variables params, n,
         freshen_term ty, freshen_name_ty_b fields)