# HG changeset patch # User haftmann # Date 1244581195 -7200 # Node ID 946a7a175bf1a1146a15122315c01f45e5f8c24f # Parent 9a59cf39ee7849d28eaf200ab206e90da5a5f5bd corrected printing of record labels diff -r 9a59cf39ee78 -r 946a7a175bf1 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Tue Jun 09 22:59:54 2009 +0200 +++ b/src/Tools/code/code_ml.ML Tue Jun 09 22:59:55 2009 +0200 @@ -311,13 +311,13 @@ let fun pr_superclass (_, (classrel, dss)) = concat [ - (str o deresolve) classrel, + (str o Long_Name.base_name o deresolve) classrel, str "=", pr_dicts NOBR [DictConst dss] ]; fun pr_classparam ((classparam, c_inst), (thm, _)) = concat [ - (str o deresolve) classparam, + (str o Long_Name.base_name o deresolve) classparam, str "=", pr_app (K false) thm reserved_names NOBR (c_inst, []) ];