diff -r 292970b42770 -r 61ee96bc9895 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sun Oct 25 19:21:34 2009 +0100
+++ b/src/Pure/codegen.ML	Sun Oct 25 20:54:21 2009 +0100
@@ -446,13 +446,8 @@
 fun map_node k f (gr, x) = (Graph.map_node k f gr, x);
 fun new_node p (gr, x) = (Graph.new_node p gr, x);
 
-fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN);
-
-fun thyname_of_type thy =
-  thyname_of thy (Type.the_tags (Sign.tsig_of thy));
-
-fun thyname_of_const thy =
-  thyname_of thy (Consts.the_tags (Sign.consts_of thy));
+fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
+fun thyname_of_const thy = #theory_name o Name_Space.the_entry (Sign.const_space thy);
 
 fun rename_terms ts =
   let