diff -r 7f7337447b1b -r e21426f244aa src/Tools/Code_Generator.thy --- a/src/Tools/Code_Generator.thy Fri May 24 23:57:24 2013 +0200 +++ b/src/Tools/Code_Generator.thy Fri May 24 23:57:24 2013 +0200 @@ -8,7 +8,7 @@ imports Pure keywords "value" "print_codeproc" "code_thms" "code_deps" :: diag and - "export_code" "code_printing" "code_class" "code_instance" "code_type" + "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type" "code_const" "code_reserved" "code_include" "code_modulename" "code_abort" "code_monad" "code_reflect" :: thy_decl and "datatypes" "functions" "module_name" "file" "checking"