# HG changeset patch
# User haftmann
# Date 1186667576 -7200
# Node ID a879b30e8e86f3a4efd3bd2a1fdd06dd6d692b4d
# Parent  adadbf9b42a457094989b36cea806669ddc69abb
proper handling of empty datatypes

diff -r adadbf9b42a4 -r a879b30e8e86 src/Pure/Tools/codegen_data.ML
--- a/src/Pure/Tools/codegen_data.ML	Thu Aug 09 15:52:55 2007 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Thu Aug 09 15:52:56 2007 +0200
@@ -680,7 +680,8 @@
   case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
    of SOME (vs, cos) => let
         val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
-      in map_exec_purge (SOME consts) (map_dtyps (Symtab.delete tyco)) thy end
+      in map_exec_purge (if null consts then NONE else SOME consts)
+        (map_dtyps (Symtab.delete tyco)) thy end
     | NONE => thy;
 
 in