diff -r d23e75d4f7da -r c859019d3ac5 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Oct 24 19:04:57 2009 +0200
+++ b/src/Pure/codegen.ML	Sat Oct 24 19:20:03 2009 +0200
@@ -337,15 +337,16 @@
     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
-          NONE => CodegenData.put {codegens = codegens,
-            tycodegens = tycodegens, consts = consts,
-            types = (tc, syn) :: types,
-            preprocs = preprocs, modules = modules} thy
-        | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
+        else
+          (case AList.lookup (op =) types tc of
+            NONE => CodegenData.put {codegens = codegens,
+              tycodegens = tycodegens, consts = consts,
+              types = (tc, syn) :: types,
+              preprocs = preprocs, modules = modules} thy
+          | SOME _ => error ("Type " ^ tc ^ " already associated with code"))
     | _ => error ("Not a type constructor: " ^ s)
   end;