diff -r 241792a4634e -r 3aa960295c54 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Wed Sep 20 12:05:31 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Wed Sep 20 12:23:54 2006 +0200
@@ -609,11 +609,13 @@
 
 fun del_datatype tyco thy =
   let
-    val SOME ((_, cs), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco
+    val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
+    val cs = mk_cos tyco vs cos;
+    val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
     val del =
       map_dtyps (Symtab.delete tyco)
-      #> map_dconstrs (fold Consttab.delete cs)
-  in map_exec_purge (SOME cs) del thy end;
+      #> map_dconstrs (fold Consttab.delete consts)
+  in map_exec_purge (SOME consts) del thy end;
 
 fun add_inline thm thy =
   map_exec_purge NONE (map_preproc (apfst (fold (insert eq_thm) (mk_rew thy thm)))) thy;