--- a/src/HOL/Codegenerator_Test/Generate.thy Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Generate.thy Fri Feb 15 11:47:34 2013 +0100
@@ -4,11 +4,12 @@
header {* Pervasive test of code generator *}
theory Generate
-imports Candidates
+imports
+ Candidates
+ "~~/src/HOL/Library/AList_Mapping"
+ "~~/src/HOL/Library/Finite_Lattice"
begin
-subsection {* Check whether generated code compiles *}
-
text {*
If any of the checks fails, inspect the code generated
by a corresponding @{text export_code} command.
@@ -17,3 +18,4 @@
export_code _ checking SML OCaml? Haskell? Scala
end
+