# HG changeset patch
# User haftmann
# Date 1372920764 -7200
# Node ID 4a884366b0d86c9c910fd55600819251dd849a6b
# Parent  598addf652090230ffb38d455bffc7902a00b060
consider explicit hint for domain of class parameters when printing instance statements

diff -r 598addf65209 -r 4a884366b0d8 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 04 08:52:44 2013 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 04 08:52:44 2013 +0200
@@ -260,17 +260,21 @@
           let
             val tyvars = intro_tyvars vs reserved;
             val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
-            fun print_classparam_instance ((classparam, (const as { dom, ... }, _)), (thm, _)) =
+            fun print_classparam_instance ((classparam, (const as { dom, ... }, dom_length)), (thm, _)) =
               let
                 val aux_dom = Name.invent_names (snd reserved) "a" dom;
                 val auxs = map fst aux_dom;
                 val vars = intro_vars auxs reserved;
-                val aux_abstr = if null auxs then [] else [enum "," "(" ")"
-                  (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
-                  (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+                val (aux_dom1, aux_dom2) = chop dom_length aux_dom;
+                fun abstract_using [] = []
+                  | abstract_using aux_dom = [enum "," "(" ")"
+                      (map (fn (aux, ty) => constraint ((str o lookup_var vars) aux)
+                      (print_typ tyvars NOBR ty)) aux_dom), str "=>"];
+                val aux_abstr1 = abstract_using aux_dom1;
+                val aux_abstr2 = abstract_using aux_dom2;
               in
                 concat ([str "val", print_method classparam, str "="]
-                  @ aux_abstr @| print_app tyvars false (SOME thm) vars NOBR
+                  @ aux_abstr1 @ aux_abstr2 @| print_app tyvars false (SOME thm) vars NOBR
                     (const, map (IVar o SOME) auxs))
               end;
           in