fixed bug
authorhaftmann
Wed Sep 20 12:23:54 2006 +0200 (2006-09-20)
changeset 206393aa960295c54
parent 20638 241792a4634e
child 20640 05e6042394b9
fixed bug
src/Pure/Tools/codegen_data.ML
     1.1 --- a/src/Pure/Tools/codegen_data.ML	Wed Sep 20 12:05:31 2006 +0200
     1.2 +++ b/src/Pure/Tools/codegen_data.ML	Wed Sep 20 12:23:54 2006 +0200
     1.3 @@ -609,11 +609,13 @@
     1.4  
     1.5  fun del_datatype tyco thy =
     1.6    let
     1.7 -    val SOME ((_, cs), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco
     1.8 +    val SOME ((vs, cos), _) = Symtab.lookup ((the_dtyps o get_exec) thy) tyco;
     1.9 +    val cs = mk_cos tyco vs cos;
    1.10 +    val consts = map (CodegenConsts.norm_of_typ thy o dest_Const o fst) cs;
    1.11      val del =
    1.12        map_dtyps (Symtab.delete tyco)
    1.13 -      #> map_dconstrs (fold Consttab.delete cs)
    1.14 -  in map_exec_purge (SOME cs) del thy end;
    1.15 +      #> map_dconstrs (fold Consttab.delete consts)
    1.16 +  in map_exec_purge (SOME consts) del thy end;
    1.17  
    1.18  fun add_inline thm thy =
    1.19    map_exec_purge NONE (map_preproc (apfst (fold (insert eq_thm) (mk_rew thy thm)))) thy;