src/HOL/Library/RType.thy

--- a/src/HOL/Library/RType.thy	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/HOL/Library/RType.thy	Mon Sep 29 10:58:01 2008 +0200
@@ -70,8 +70,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;
 
 fun perhaps_add_def tyco thy =