# HG changeset patch
# User haftmann
# Date 1219581746 -7200
# Node ID 00e005cdceb0d34cb55069f78a3154346fc2caee
# Parent  2aaa4a5569a6c45fa8a96c9534e30a5a0e2ff7fc
corrected cache handling for class operations

diff -r 2aaa4a5569a6 -r 00e005cdceb0 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Aug 24 14:42:24 2008 +0200
+++ b/src/Pure/Isar/code.ML	Sun Aug 24 14:42:26 2008 +0200
@@ -354,9 +354,14 @@
 
 val the_exec = fst o CodeData.get;
 
+fun complete_class_params thy cs =
+  fold (fn c => case AxClass.inst_of_param thy c
+   of NONE => insert (op =) c
+    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
+
 fun map_exec_purge touched f thy =
   CodeData.map (fn (exec, data) => (f exec, ref (case touched
-   of SOME cs => invoke_purge_all thy cs (! data)
+   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
     | NONE => empty_data))) thy;
 
 val purge_data = (CodeData.map o apsnd) (K (ref empty_data));