# HG changeset patch
# User haftmann
# Date 1587734200 0
# Node ID fc4f9dad52924cd67154d6967763d9268d957224
# Parent  54d4bfa48025fe6f9f1707da0b4463da519520b3
opaque export does not work as expected in presence of dependent instances

diff -r 54d4bfa48025 -r fc4f9dad5292 src/Tools/Code/code_ml.ML
--- 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*)