src/Tools/Code/code_scala.ML
changeset 77707 a6a81f848135
parent 77703 0262155d2743
child 78594 1cce41dc0c41
--- a/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
+++ b/src/Tools/Code/code_scala.ML	Fri Mar 24 18:30:17 2023 +0000
@@ -75,7 +75,7 @@
       | print_var vars (SOME v) = (str o lookup_var vars) v;
     fun applify_dict tyvars (Dict (_, d)) = applify_plain_dict tyvars d
     and applify_plain_dict tyvars (Dict_Const (inst, dss)) =
-          applify_dictss tyvars ((str o deresolve o Class_Instance) inst) dss
+          applify_dictss tyvars ((str o deresolve o Class_Instance) inst) (map snd dss)
       | applify_plain_dict tyvars (Dict_Var { var, class, ... }) =
           Pretty.block [str "implicitly",
             enclose "[" "]" [Pretty.block [(str o deresolve_class) class,