diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_names.ML
--- a/src/Pure/Tools/codegen_names.ML	Thu Jan 25 09:32:50 2007 +0100
+++ b/src/Pure/Tools/codegen_names.ML	Thu Jan 25 09:32:51 2007 +0100
@@ -261,7 +261,7 @@
     | NONE => (case CodegenData.get_datatype_of_constr thy const
    of SOME dtco => SOME (thyname_of_tyco thy dtco)
     | NONE => (case CodegenConsts.find_def thy const
-   of SOME ((thyname, _), _) => SOME thyname
+   of SOME (thyname, _) => SOME thyname
     | NONE => NONE));
 
 fun const_policy thy (c, tys) =