diff --git a/src/Pure/System/scala_compiler.ML b/src/Pure/System/scala_compiler.ML
--- a/src/Pure/System/scala_compiler.ML
+++ b/src/Pure/System/scala_compiler.ML
@@ -1,85 +1,85 @@
 (*  Title:      Pure/System/scala_compiler.ML
     Author:     Makarius
 
 Scala compiler operations.
 *)
 
 signature SCALA_COMPILER =
 sig
   val toplevel: string -> unit
-  val declaration: string -> unit
+  val static_check: string -> unit
 end;
 
 structure Scala_Compiler: SCALA_COMPILER =
 struct
 
 (* check declaration *)
 
 fun toplevel source =
   let val errors =
     \<^scala>\<open>scala_toplevel\<close> source
     |> YXML.parse_body
     |> let open XML.Decode in list string end
   in if null errors then () else error (cat_lines errors) end;
 
-fun declaration source =
-  toplevel ("package test\nobject Test { " ^ source ^ " }");
+fun static_check source =
+  toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }");
 
 
 (* antiquotations *)
 
 local
 
 fun make_list bg en = space_implode "," #> enclose bg en;
 
 fun print_args [] = ""
   | print_args xs = make_list "(" ")" xs;
 
 fun print_types [] = ""
   | print_types Ts = make_list "[" "]" Ts;
 
 fun print_class (c, Ts) = c ^ print_types Ts;
 
 val types =
   Scan.optional (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]") [];
 
 val in_class =
   Parse.$$$ "(" |-- Parse.!!! (Parse.$$$ "in" |-- Parse.name -- types  --| Parse.$$$ ")");
 
 val arguments =
   (Parse.nat >> (fn n => replicate n "_") ||
     Parse.list (Parse.underscore || Parse.name >> (fn T => "_ : " ^ T))) >> print_args
   || Scan.succeed " _";
 
 val method_arguments = Scan.optional (Parse.$$$ "(" |-- arguments --| Parse.$$$ ")") " _";
 
 in
 
 val _ =
   Theory.setup
     (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_type\<close>
       (Scan.lift (Parse.embedded -- (types >> print_types)))
       (fn _ => fn (t, type_args) =>
-        (declaration ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #>
+        (static_check ("type _Test_" ^ type_args ^ " = " ^ t ^ type_args); t ^ type_args)) #>
 
     Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_object\<close>
       (Scan.lift Parse.embedded)
-      (fn _ => fn object => (declaration ("val _test_ = " ^ object); object)) #>
+      (fn _ => fn object => (static_check ("val _test_ = " ^ object); object)) #>
 
     Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>scala_method\<close>
       (Scan.lift (Scan.option in_class -- Parse.embedded -- types -- method_arguments))
       (fn _ => fn (((class, method), method_types), method_args) =>
         let
           val class_types = (case class of SOME (_, Ts) => Ts | NONE => []);
           val def = "def _test_" ^ print_types (merge (op =) (method_types, class_types));
           val def_context =
             (case class of
               NONE => def ^ " = "
             | SOME c => def ^ "(_this_ : " ^ print_class c ^ ") = _this_.");
           val source = def_context ^ method ^ method_args;
-          val _ = declaration source;
+          val _ = static_check source;
         in (case class of NONE => method | SOME c => print_class c ^ "." ^ method) end));
 
 end;
 
 end;