X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=d9ba51db066a8001f7bcfc01b486618e13afb3b5;hb=95e3387af669e9a9e30dafd4d096c2741fc9041c;hp=8828a03216bb74c64b71db833276fdd8c500d662;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 8828a0321..d9ba51db0 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -317,7 +317,7 @@ let pp_obj pp_term = function
             (pp_term typ) (pp_constructors constructors)
         in
         fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (flavour, name, typ, body,_) ->
+ | Ast.Theorem (name, typ, body,(_,flavour,_)) ->
     sprintf "%s %s:\n %s\n%s"
       (NCicPp.string_of_flavour flavour)
       name