diff -r ed9be131a4ec -r 5aae37575885 src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:09 2010 +0200
+++ b/src/Tools/Code/code_target.ML	Wed Apr 28 15:17:13 2010 +0200
@@ -6,6 +6,9 @@
 
 signature CODE_TARGET =
 sig
+  val cert_tyco: theory -> string -> string
+  val read_tyco: theory -> string -> string
+
   type serializer
   type literals = Code_Printer.literals
   val add_target: string * (serializer * literals) -> theory -> theory