dropped now obsolete purge_data -- happens implicitly on change of theory identity
--- a/src/Pure/Isar/code.ML Sun Aug 22 14:27:30 2010 +0200
+++ b/src/Pure/Isar/code.ML Mon Aug 23 11:09:48 2010 +0200
@@ -78,7 +78,6 @@
(*infrastructure*)
val set_code_target_attr: (string -> thm -> theory -> theory) -> theory -> theory
- val purge_data: theory -> theory
end;
signature CODE_DATA_ARGS =
@@ -266,8 +265,6 @@
fun map_exec_purge f = Code_Data.map (fn (exec, _) => (f exec, empty_dataref ()));
-val purge_data = (Code_Data.map o apsnd) (fn _ => 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), [])))
o apfst) (fn (_, spec) => (true, f spec));