1.1 --- a/src/Pure/Isar/named_target.ML	Thu Aug 12 09:00:19 2010 +0200
     1.2 +++ b/src/Pure/Isar/named_target.ML	Thu Aug 12 13:23:46 2010 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val peek: local_theory -> {target: string, is_locale: bool, is_class: bool}
     1.6    val init: string option -> theory -> local_theory
     1.7 +  val theory_init: theory -> local_theory
     1.8    val context_cmd: xstring -> theory -> local_theory
     1.9  end;
    1.10  
    1.11 @@ -202,6 +203,8 @@
    1.12  
    1.13  fun init target thy = init_target (named_target thy target) thy;
    1.14  
    1.15 +val theory_init = init_target global_target;
    1.16 +
    1.17  fun context_cmd "-" thy = init NONE thy
    1.18    | context_cmd target thy = init (SOME (Locale.intern thy target)) thy;
    1.19