diff -r a56099a6447a -r eedd549de3ef src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sun Jan 26 14:01:19 2014 +0100
+++ b/src/Tools/Code/code_scala.ML	Sun Jan 26 16:23:46 2014 +0100
@@ -89,11 +89,11 @@
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR ((str o deresolve) sym) typargs') ts)
-          | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
+          | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")"
               (print_term tyvars is_pat some_thm vars NOBR) fxy
                 (applify "[" "]" (print_typ tyvars NOBR)
                   NOBR (str s) typargs') ts)
-          | SOME (Complex_const_syntax (k, print)) =>
+          | SOME (k, Complex_printer print) =>
               (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
                 (ts ~~ take k dom))
       in if k = l then print' fxy ts