diff -r b47d41d9f4b5 -r 6ca5407863ed src/Tools/Code/code_target.ML
--- a/src/Tools/Code/code_target.ML	Sat Apr 16 13:48:45 2011 +0200
+++ b/src/Tools/Code/code_target.ML	Sat Apr 16 15:25:25 2011 +0200
@@ -307,13 +307,16 @@
 
 fun project_program thy abortable names_hidden names1 program2 =
   let
+    val ctxt = ProofContext.init_global thy;
     val names2 = subtract (op =) names_hidden names1;
     val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
     val names4 = Graph.all_succs program3 names2;
     val empty_funs = filter_out (member (op =) abortable)
       (Code_Thingol.empty_funs program3);
-    val _ = if null empty_funs then () else error ("No code equations for "
-      ^ commas (map (Sign.extern_const thy) empty_funs));
+    val _ =
+      if null empty_funs then ()
+      else error ("No code equations for " ^
+        commas (map (ProofContext.extern_const ctxt) empty_funs));
     val program4 = Graph.subgraph (member (op =) names4) program3;
   in (names4, program4) end;