diff -r 599ff65b85e2 -r 6ed12ae3b3e1 src/HOL/Codegenerator_Test/Generate.thy
--- 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
+