diff -r bf7d82193a2e -r 8d12ac6a3e1c src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Jun 20 21:00:25 2008 +0200
+++ b/src/Pure/codegen.ML	Fri Jun 20 21:00:26 2008 +0200
@@ -388,7 +388,7 @@
     val tc = Sign.intern_type thy s;
   in
     case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of
-      SOME (Type.LogicalType i, _) =>
+      SOME ((Type.LogicalType i, _), _) =>
         if num_args_of (fst syn) > i then
           error ("More arguments than corresponding type constructor " ^ s)
         else (case AList.lookup (op =) types tc of