- ng_refiner:

[helm.git] / matita / components / content / notationPp.ml

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 8828a03216bb74c64b71db833276fdd8c500d662..d9ba51db066a8001f7bcfc01b486618e13afb3b5 100644 (file)
--- 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