diff -r 30ba169e8c45 -r b9c8e3a12a98 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Sep 28 14:46:51 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Sep 29 10:58:01 2008 +0200
@@ -109,7 +109,7 @@
 type generic_theory = Context.generic;    (*theory or local_theory*)
 
 val loc_init = TheoryTarget.context;
-val loc_exit = ProofContext.theory_of o LocalTheory.exit;
+val loc_exit = LocalTheory.exit_global;
 
 fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy
   | loc_begin NONE (Context.Proof lthy) = lthy