src/Pure/Isar/code.ML

 
 val the_exec : theory -> spec = fst o Code_Data.get;
 
 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));
 
 
 (* tackling equation history *)
 

     fun add_eqn' true (Default (eqns, _)) = Default (natural_order ((thm, proper) :: eqns))
           (*this restores the natural order and drops syntactic redundancies*)
       | 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;
 
 fun add_nbe_eqn thm thy =

  of SOME (thm, _) => let
         fun del_eqn' (Default _) = empty_fun_spec
           | 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 *)
 
 fun case_cong thy case_const (num_args, (pos, _)) =

     val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
       error_abs_thm (check_abstype_cert thy) thy proto_thm;
   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;