author | haftmann |
Sat, 25 Apr 2020 13:26:25 +0000 | |
changeset 71803 | 14914ae80f70 |
parent 71802 | ab3cecb836b5 |
child 71804 | 6fd70ed18199 |
--- a/src/Tools/Code/code_ml.ML Sat Apr 25 13:26:24 2020 +0000 +++ b/src/Tools/Code/code_ml.ML Sat Apr 25 13:26:25 2020 +0000 @@ -692,7 +692,7 @@ ) ]; in pair - (if Code_Namespace.not_private export + (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*)