src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 07:55:46 2007 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Thu Nov 29 17:08:26 2007 +0100
@@ -544,7 +544,7 @@
         |> not (null arities) ? (
             f arities css
             #-> (fn defs =>
-              Class.prove_instance tac arities defs
+              Instance.prove_instance tac arities defs
             #-> (fn defs =>
               after_qed arities css defs)))
       end;