diff -r 3daaf23b9ab4 -r 6315b6426200 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Thu Jul 08 16:19:24 2010 +0200
@@ -7,9 +7,23 @@
 imports Candidates
 begin
 
-export_code * in SML module_name Code_Test
-  in OCaml module_name Code_Test file -
-  in Haskell file -
-  in Scala file -
+subsection {* Check whether generated code compiles *}
+
+text {*
+  If any of the @{text ML} ... check fails, inspect the code generated
+  by the previous @{text export_code} command.
+*}
+
+export_code "*" in SML module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_SML @{theory}) *}
+
+export_code "*" in OCaml module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_ML.check_OCaml @{theory}) *}
+
+export_code "*" in Haskell module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Haskell.check @{theory}) *}
+
+export_code "*" in Scala module_name Code_Test file -
+ML {* Cache_IO.with_tmp_dir "Code_Test" (Code_Scala.check @{theory}) *}
 
 end