--- 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);