# HG changeset patch
# User haftmann
# Date 1275673001 -7200
# Node ID c0cf8b6c2c26b6e332ddd71ae9ea172bfec88879
# Parent  a05d0c1b0cb3b46eb68203ec4d2dfdc860d74693
avoid "$"

diff -r a05d0c1b0cb3 -r c0cf8b6c2c26 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Fri Jun 04 19:36:40 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Fri Jun 04 19:36:41 2010 +0200
@@ -228,7 +228,7 @@
                   concat [enum "," "(" ")" (map (print_typ tyvars NOBR) tys),
                     str "=>", print_typ tyvars NOBR ty];
             fun print_classparam_val (classparam, ty) =
-              concat [str "val", (str o suffix "$:" o deresolve_base) classparam,
+              concat [str "val", (str o Library.enclose "`" "+`:" o deresolve_base) classparam,
                 (print_tupled_typ o Code_Thingol.unfold_fun) ty]
             fun print_classparam_def (classparam, ty) =
               let
@@ -239,7 +239,7 @@
                 val head = print_defhead tyvars vars' ((str o deresolve) classparam) vs params tys [p_implicit] ty;
               in
                 concat [head, applify "(" ")" NOBR
-                  (Pretty.block [str implicit, str ".", (str o suffix "$" o deresolve_base) classparam])
+                  (Pretty.block [str implicit, str ".", (str o Library.enclose "`" "+`" o deresolve_base) classparam])
                   (map (str o lookup_var vars') params)]
               end;
           in
@@ -268,7 +268,7 @@
                   [concat [enum "," "(" ")" (map2 (fn aux => fn ty => print_typed tyvars ((str o lookup_var vars) aux) ty)
                     auxs tys), str "=>"]];
               in 
-                concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
+                concat ([str "val", (str o Library.enclose "`" "+`" o deresolve_base) classparam,
                   str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
               end;
           in