src/Tools/Code/code_ml.ML
changeset 71798 fc4f9dad5292
parent 70352 ce3c1d8791eb
child 71803 14914ae80f70
equal deleted inserted replaced
71797:54d4bfa48025 71798:fc4f9dad5292
   690                   map print_super_class_field classrels
   690                   map print_super_class_field classrels
   691                   @ map print_classparam_field classparams
   691                   @ map print_classparam_field classparams
   692                 )
   692                 )
   693               ];
   693               ];
   694           in pair
   694           in pair
   695            (if Code_Namespace.is_public export
   695            (if Code_Namespace.not_private export
   696               then type_decl_p :: map print_classparam_decl classparams
   696               then type_decl_p :: map print_classparam_decl classparams
   697               else if null classrels andalso null classparams
   697               else if null classrels andalso null classparams
   698               then [type_decl_p] (*work around weakness in export calculation*)
   698               then [type_decl_p] (*work around weakness in export calculation*)
   699               else [concat [str "type", print_dicttyp (class, ITyVar v)]])
   699               else [concat [str "type", print_dicttyp (class, ITyVar v)]])
   700             (Pretty.chunks (
   700             (Pretty.chunks (