src/HOL/Tools/datatype_codegen.ML

--- a/src/HOL/Tools/datatype_codegen.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -471,8 +471,7 @@
     |> TheoryTarget.instantiation (dtcos, vs', [HOLogic.class_eq])
     |> fold_map add_def dtcos
     |-> (fn thms => Class.prove_instantiation_instance (K (tac thms))
-    #> LocalTheory.exit
-    #> ProofContext.theory_of
+    #> LocalTheory.exit_global
     #> fold Code.del_eqn thms
     #> fold add_eq_thms dtcos)
   end;