--- a/src/Tools/Code/code_scala.ML Wed Jan 24 11:56:38 2018 +0100
+++ b/src/Tools/Code/code_scala.ML Wed Jan 24 11:56:54 2018 +0100
@@ -460,7 +460,7 @@
make_destination = fn p => Path.append p (Path.explode "ROOT.scala"),
make_command = fn _ =>
"isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS ROOT.scala"},
- evaluation_args = Token.explode Keyword.empty_keywords @{here} "case_insensitive"})
+ evaluation_args = Token.explode0 Keyword.empty_keywords "case_insensitive"})
#> Code_Target.set_printings (Type_Constructor ("fun",
[(target, SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (