src/HOL/Typedef.thy

--- a/src/HOL/Typedef.thy	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Typedef.thy	Mon Sep 29 10:58:01 2008 +0200
@@ -148,8 +148,7 @@
     |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
     |> snd
     |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
-    |> LocalTheory.exit
-    |> ProofContext.theory_of
+    |> LocalTheory.exit_global
   end
 in TypedefPackage.interpretation add_itself end
 *}