--- a/src/Pure/Isar/code.ML Mon Jul 21 15:26:25 2008 +0200
+++ b/src/Pure/Isar/code.ML Mon Jul 21 15:26:26 2008 +0200
@@ -30,6 +30,7 @@
-> theory -> theory) -> theory -> theory
val add_case: thm -> theory -> theory
val add_undefined: string -> theory -> theory
+ val purge_data: theory -> theory
val coregular_algebra: theory -> Sorts.algebra
val operational_algebra: theory -> (sort -> sort) * Sorts.algebra
@@ -358,6 +359,8 @@
of SOME cs => invoke_purge_all thy cs (! data)
| NONE => empty_data))) thy;
+val purge_data = (CodeData.map o apsnd) (K (ref empty_data));
+
(* access to data dependent on abstract executable content *)