tuned;

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