diff -r 9cde57cdd0e3 -r 8494cb38cbf7 src/Pure/Isar/code.ML
--- 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));