X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent%2FnotationPp.ml;h=59df4ffddb3204e074a3c4366949fc12260fa9ed;hb=0d2bfb98d8343b4e6cefdb506a813b7cb5749630;hp=30abf348eda3b10e45941f096e31b50e26f9b7d7;hpb=cb11de1c61f0b61935b1c6c1832deacb49f7b5bd;p=helm.git

diff --git a/matita/components/content/notationPp.ml b/matita/components/content/notationPp.ml
index 30abf348e..59df4ffdd 100644
--- a/matita/components/content/notationPp.ml
+++ b/matita/components/content/notationPp.ml
@@ -279,17 +279,6 @@ let pp_params pp_term = function
   | [] -> ""
   | params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params)
       
-let pp_flavour = function
-  | `Definition -> "definition"
-  | `MutualDefinition -> assert false
-  | `Fact -> "fact"
-  | `Goal -> "goal"
-  | `Lemma -> "lemma"
-  | `Remark -> "remark"
-  | `Theorem -> "theorem"
-  | `Variant -> "variant"
-  | `Axiom -> "axiom"
-
 let pp_fields pp_term fields =
   (if fields <> [] then "\n" else "") ^ 
   String.concat ";\n" 
@@ -322,11 +311,9 @@ 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 (`MutualDefinition, name, typ, body,_) ->
-    sprintf "<<pretty printing of mutual definitions not implemented yet>>"
  | Ast.Theorem (flavour, name, typ, body,_) ->
     sprintf "%s %s:\n %s\n%s"
-      (pp_flavour flavour)
+      (NCicPp.string_of_flavour flavour)
       name
       (pp_term typ)
       (match body with