# HG changeset patch
# User haftmann
# Date 1244444571 -7200
# Node ID e2de58666d21df421ad3e428274c65b4003c0fae
# Parent  eced346b2231081e544236f15ed8a4f00f003cde
proper deresolving of class relations and class parameters in SML

diff -r eced346b2231 -r e2de58666d21 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Mon Jun 08 00:26:57 2009 +0200
+++ b/src/Tools/code/code_ml.ML	Mon Jun 08 09:02:51 2009 +0200
@@ -47,9 +47,6 @@
 
 fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
   let
-    val pr_label_classrel = translate_string (fn "." => "__" | c => c)
-      o Long_Name.qualifier;
-    val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = Code_Printer.first_upper v ^ "_"
@@ -272,11 +269,11 @@
             val w = Code_Printer.first_upper v ^ "_";
             fun pr_superclass_field (class, classrel) =
               (concat o map str) [
-                pr_label_classrel classrel, ":", "'" ^ v, deresolve class
+                deresolve classrel, ":", "'" ^ v, deresolve class
               ];
             fun pr_classparam_field (classparam, ty) =
               concat [
-                (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
+                (str o deresolve) classparam, str ":", pr_typ NOBR ty
               ];
             fun pr_classparam_proj (classparam, _) =
               semicolon [
@@ -284,7 +281,7 @@
                 (str o deresolve) classparam,
                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
                 str "=",
-                str ("#" ^ pr_label_classparam classparam),
+                str ("#" ^ deresolve classparam),
                 str w
               ];
             fun pr_superclass_proj (_, classrel) =
@@ -293,7 +290,7 @@
                 (str o deresolve) classrel,
                 Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
                 str "=",
-                str ("#" ^ pr_label_classrel classrel),
+                str ("#" ^ deresolve classrel),
                 str w
               ];
           in
@@ -314,13 +311,13 @@
           let
             fun pr_superclass (_, (classrel, dss)) =
               concat [
-                (str o pr_label_classrel) classrel,
+                (str o deresolve) classrel,
                 str "=",
                 pr_dicts NOBR [DictConst dss]
               ];
             fun pr_classparam ((classparam, c_inst), (thm, _)) =
               concat [
-                (str o pr_label_classparam) classparam,
+                (str o deresolve) classparam,
                 str "=",
                 pr_app (K false) thm reserved_names NOBR (c_inst, [])
               ];