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 #>