# HG changeset patch
# User haftmann
# Date 1242035601 -7200
# Node ID 8316d22f10f569eaa0afceaf2758a27a36447804
# Parent  3be41b2710236512714a0fb73c8bbe9e8df6a29b
corrected deletetion of code equations for constructors

diff -r 3be41b271023 -r 8316d22f10f5 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon May 11 10:53:19 2009 +0200
+++ b/src/Pure/Isar/code.ML	Mon May 11 11:53:21 2009 +0200
@@ -541,9 +541,9 @@
           then insert (op =) c else I) cases []) cases;
   in
     thy
+    |> fold (del_eqns o fst) cs
     |> map_exec_purge NONE
         ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
-        #> map_eqns (fold (Symtab.delete_safe o fst) cs)
         #> (map_cases o apfst) drop_outdated_cases)
     |> TypeInterpretation.data (tyco, serial ())
   end;