diff -r 4301e9ea1c54 -r 458ced35abb8 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:14 2009 +0100
+++ b/src/Tools/Code/code_preproc.ML	Wed Dec 23 08:31:15 2009 +0100
@@ -445,22 +445,10 @@
 
 (** store for preprocessed arities and code equations **)
 
-structure Wellsorted = Code_Data_Fun
+structure Wellsorted = Code_Data
 (
   type T = ((string * class) * sort list) list * code_graph;
   val empty = ([], Graph.empty);
-  fun purge thy cs (arities, eqngr) =
-    let
-      val del_cs = ((Graph.all_preds eqngr
-        o filter (can (Graph.get_node eqngr))) cs);
-      val del_arities = del_cs
-        |> map_filter (AxClass.inst_of_param thy)
-        |> maps (fn (c, tyco) =>
-             (map (rpair tyco) o Sign.complete_sort thy o the_list
-               o AxClass.class_of_param thy) c);
-      val arities' = fold (AList.delete (op =)) del_arities arities;
-      val eqngr' = Graph.del_nodes del_cs eqngr;
-    in (arities', eqngr') end;
 );