# 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, [])
               ];