src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Thu Aug 02 23:18:13 2007 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Fri Aug 03 16:28:15 2007 +0200
@@ -596,7 +596,7 @@
   let
     fun add_eq_thms (dtco, (_, (vs, cs))) thy =
       let
-        val thy_ref = Theory.self_ref thy;
+        val thy_ref = Theory.check_thy thy;
         val const = ("op =", SOME dtco);
         val get_thms = (fn () => get_eq (Theory.deref thy_ref) dtco |> rev);
       in