# HG changeset patch
# User haftmann
# Date 1388534730 -3600
# Node ID 3774542df61bb6a21d0c7659cfe3e1f727410786
# Parent  3a478d0a0e8736d9d16cc2ecc8cc511544d0a856
uniform bookkeeping also in the case of deletion

diff -r 3a478d0a0e87 -r 3774542df61b src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Tue Dec 31 22:18:31 2013 +0100
+++ b/src/Pure/Isar/code.ML	Wed Jan 01 01:05:30 2014 +0100
@@ -294,8 +294,8 @@
 
 fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
 
-fun change_fun_spec delete c f = (map_exec_purge o map_functions
-  o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
+fun change_fun_spec c f = (map_exec_purge o map_functions
+  o (Symtab.map_default (c, ((false, empty_fun_spec), [])))
     o apfst) (fn (_, spec) => (true, f spec));
 
 
@@ -1057,13 +1057,13 @@
       | add_eqn' true fun_spec = fun_spec
       | add_eqn' false (Eqns eqns) = Eqns (update_subsume true (thm, proper) eqns)
       | add_eqn' false _ = Eqns [(thm, proper)];
-  in change_fun_spec false c (add_eqn' default) thy end;
+  in change_fun_spec c (add_eqn' default) thy end;
 
 fun gen_add_abs_eqn raw_thm thy =
   let
     val (abs_thm, tyco) = apfst Thm.close_derivation raw_thm;
     val c = const_abs_eqn thy abs_thm;
-  in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end;
+  in change_fun_spec c (K (Abstr (abs_thm, tyco))) thy end;
 
 fun add_eqn thm thy =
   gen_add_eqn false (mk_eqn thy (thm, true)) thy;
@@ -1101,10 +1101,10 @@
           | del_eqn' (Eqns eqns) =
               Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
           | del_eqn' spec = spec
-      in change_fun_spec true (const_eqn thy thm) del_eqn' thy end
+      in change_fun_spec (const_eqn thy thm) del_eqn' thy end
   | NONE => thy;
 
-fun del_eqns c = change_fun_spec true c (K empty_fun_spec);
+fun del_eqns c = change_fun_spec c (K empty_fun_spec);
 
 
 (* cases *)
@@ -1217,7 +1217,7 @@
   in
     thy
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
-    |> change_fun_spec false rep
+    |> change_fun_spec rep
       (K (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs rep), tyco)))
     |> Abstype_Interpretation.data (tyco, serial ())
   end;