diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Wed Jul 14 15:08:02 2010 +0200
@@ -7,7 +7,6 @@
 signature CODE_SCALA =
 sig
   val target: string
-  val check: theory -> unit
   val setup: theory -> theory
 end;
 
@@ -414,14 +413,6 @@
 } end;
 
 
-(** formal checking of compiled code **)
-
-fun check thy = Code_Target.external_check thy target
-  "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
-    Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
-
-
-
 (** Isar setup **)
 
 fun isar_serializer module_name =
@@ -430,7 +421,10 @@
 
 val setup =
   Code_Target.add_target
-    (target, { serializer = isar_serializer, literals = literals, check = () })
+    (target, { serializer = isar_serializer, literals = literals,
+      check = { env_var = "SCALA_HOME", make_destination = I,
+        make_command = fn scala_home => fn p => fn _ =>
+          Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
   #> Code_Target.add_syntax_tyco target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (