src/Tools/Code/code_ml.ML
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]