src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Mon Dec 10 11:24:14 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Dec 10 11:24:15 2007 +0100
@@ -342,7 +342,7 @@
     |> MetaSimplifier.rewrite_rule [(Thm.symmetric o Thm.assume) asm]
     |> Thm.implies_intr asm
     |> Thm.generalize ([], params) 0
-    |> Class.unoverload thy
+    |> AxClass.unoverload thy
     |> Thm.varifyT
   end;
 
@@ -426,7 +426,7 @@
     fun add_eq_thms dtco thy =
       let
         val thy_ref = Theory.check_thy thy;
-        val const = Class.param_of_inst thy ("op =", dtco);
+        val const = AxClass.param_of_inst thy ("op =", dtco);
         val get_thms = (fn () => get_eq' (Theory.deref thy_ref) dtco |> rev);
       in
         Code.add_funcl (const, Susp.delay get_thms) thy