diff -r 370712dd4628 -r 94d5624dd1f7 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Thu Aug 12 09:00:19 2010 +0200
+++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
@@ -9,6 +9,7 @@
 sig
   val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
   val init: string option -> theory -> local_theory
+  val theory_init: theory -> local_theory
   val context_cmd: xstring -> theory -> local_theory
 end;
 
@@ -202,6 +203,8 @@
 
 fun init target thy = init_target (named_target thy target) thy;
 
+val theory_init = init_target global_target;
+
 fun context_cmd "-" thy = init NONE thy
   | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;