author | haftmann |
Fri, 24 Apr 2020 13:16:40 +0000 | |
changeset 71798 | fc4f9dad5292 |
parent 71797 | 54d4bfa48025 |
child 71799 | e00712b4e2c2 |
--- a/src/Tools/Code/code_ml.ML Thu Apr 23 23:12:20 2020 +0200 +++ b/src/Tools/Code/code_ml.ML Fri Apr 24 13:16:40 2020 +0000 @@ -692,7 +692,7 @@ ) ]; in pair - (if Code_Namespace.is_public export + (if Code_Namespace.not_private 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*)