1.1 --- a/src/Pure/Isar/theory_target.ML	Tue Nov 06 22:50:37 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Nov 06 22:50:38 2007 +0100
     1.3 @@ -305,8 +305,9 @@
     1.4    | init_target thy (SOME target) = make_target target true (Class.is_class thy target);
     1.5  
     1.6  fun init_ctxt (Target {target, is_locale, is_class}) =
     1.7 -  if is_locale then if is_class then Class.init target
     1.8 -    else Locale.init target else ProofContext.init;
     1.9 +  if not is_locale then ProofContext.init
    1.10 +  else if not is_class then Locale.init target
    1.11 +  else Class.init target;
    1.12  
    1.13  fun init_lthy (ta as Target {target, ...}) =
    1.14    Data.put ta #>