corrected cache handling for class operations

--- 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));