proper handling of empty datatypes
authorhaftmann
Thu Aug 09 15:52:56 2007 +0200 (2007-08-09)
changeset 24201a879b30e8e86
parent 24200 adadbf9b42a4
child 24202 9e77397eba8e
proper handling of empty datatypes
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/Pure/Tools/codegen_data.ML	Thu Aug 09 15:52:55 2007 +0200
     1.2 +++ b/src/Pure/Tools/codegen_data.ML	Thu Aug 09 15:52:56 2007 +0200
     1.3 @@ -680,7 +680,8 @@
     1.4    case Symtab.lookup ((the_dtyps o get_exec) thy) tyco
     1.5     of SOME (vs, cos) => let
     1.6          val consts = CodegenConsts.consts_of_cos thy tyco vs cos;
     1.7 -      in map_exec_purge (SOME consts) (map_dtyps (Symtab.delete tyco)) thy end
     1.8 +      in map_exec_purge (if null consts then NONE else SOME consts)
     1.9 +        (map_dtyps (Symtab.delete tyco)) thy end
    1.10      | NONE => thy;
    1.11  
    1.12  in