# HG changeset patch
# User haftmann
# Date 1393148023 -3600
# Node ID def6575032dff7e805642d7d5610b77ed65e7dbc
# Parent  7714287dc04486febf65e46c010886bbcad622bc
tuned

diff -r 7714287dc044 -r def6575032df src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Tools/Code/code_ml.ML	Sun Feb 23 10:33:43 2014 +0100
@@ -658,8 +658,8 @@
               (concat o map str) ["let", deresolve_const classparam, w, "=",
                 w ^ "." ^ deresolve_const classparam ^ ";;"];
             val type_decl_p = concat [
-                str ("type '" ^ v),
-                (str o deresolve_class) class,
+                str "type",
+                print_dicttyp (class, ITyVar v),
                 str "=",
                 enum_default "unit" ";" "{" "}" (
                   map print_super_class_field classrels