# HG changeset patch
# User wenzelm
# Date 1194385838 -3600
# Node ID 618247e82f3d24ccbfb8bb72c87edaa813410f55
# Parent  074d4117655849750b95633dfb2e173e5a5e8812
tuned;

diff -r 074d41176558 -r 618247e82f3d src/Pure/Isar/theory_target.ML
--- 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 #>