# HG changeset patch
# User wenzelm
# Date 1160861156 -7200
# Node ID 4b52b23f50ebdeb12fbee54b150291c451279d53
# Parent  0eed532acfca7cd5e1c97cd9fe94cff23326be7b
added peek;

diff -r 0eed532acfca -r 4b52b23f50eb src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Oct 14 23:25:55 2006 +0200
+++ b/src/Pure/Isar/theory_target.ML	Sat Oct 14 23:25:56 2006 +0200
@@ -205,6 +205,7 @@
 (* init and exit *)
 
 fun begin loc =
+  Data.put (if loc = "" then NONE else SOME loc) #>
   LocalTheory.init (SOME (NameSpace.base loc))
    {pretty = pretty loc,
     consts = consts loc,
@@ -213,8 +214,7 @@
     notes = notes loc,
     term_syntax = term_syntax loc,
     declaration = declaration loc,
-    exit = K I}
-  #> Data.put (SOME loc);
+    exit = K I};
 
 fun init_i NONE thy = begin "" (ProofContext.init thy)
   | init_i (SOME loc) thy = begin loc (Locale.init loc thy);