# HG changeset patch
# User haftmann
# Date 1216646786 -7200
# Node ID cb0021d56e119b53110f987e438e7cc19eaaae61
# Parent  2736967f27fdf5c197c8e9261af93c56251b597e
added explicit purge_data

diff -r 2736967f27fd -r cb0021d56e11 src/Pure/Isar/code.ML
--- 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 *)