# 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