# HG changeset patch
# User haftmann
# Date 1587821185 0
# Node ID 14914ae80f705666f2a8b31411f17959bf109b54
# Parent  ab3cecb836b557c0b1cf388ce9b29d61e57a89e1
temporarily revert change which does not work as expected

diff -r ab3cecb836b5 -r 14914ae80f70 src/Tools/Code/code_ml.ML
--- 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*)