1.1 --- a/src/Pure/Isar/code.ML	Sun Aug 24 14:42:24 2008 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Aug 24 14:42:26 2008 +0200
     1.3 @@ -354,9 +354,14 @@
     1.4  
     1.5  val the_exec = fst o CodeData.get;
     1.6  
     1.7 +fun complete_class_params thy cs =
     1.8 +  fold (fn c => case AxClass.inst_of_param thy c
     1.9 +   of NONE => insert (op =) c
    1.10 +    | SOME (c', _) => insert (op =) c' #> insert (op =) c) cs [];
    1.11 +
    1.12  fun map_exec_purge touched f thy =
    1.13    CodeData.map (fn (exec, data) => (f exec, ref (case touched
    1.14 -   of SOME cs => invoke_purge_all thy cs (! data)
    1.15 +   of SOME cs => invoke_purge_all thy (complete_class_params thy cs) (! data)
    1.16      | NONE => empty_data))) thy;
    1.17  
    1.18  val purge_data = (CodeData.map o apsnd) (K (ref empty_data));