| changeset 66325 | fd28cb6e6f2c |
| parent 63303 | 7cffe366d333 |
| child 66326 | 9eb8a2d07852 |
--- a/src/Tools/Code/code_ml.ML Thu Aug 03 12:49:55 2017 +0200 +++ b/src/Tools/Code/code_ml.ML Thu Aug 03 12:49:57 2017 +0200 @@ -676,6 +676,8 @@ in pair (if Code_Namespace.is_public export then type_decl_p :: map print_classparam_decl classparams + else if null classrels andalso null classparams + then [type_decl_p] (*work around weakness in export calculation*) else [concat [str "type", print_dicttyp (class, ITyVar v)]]) (Pretty.chunks ( doublesemicolon [type_decl_p]