# HG changeset patch
# User haftmann
# Date 1233579383 -3600
# Node ID f2e70a0636b9867ba44adf21fdea4c788fdccdd7
# Parent  cf8476cc440d253e07552ea2be3f64d29c13b6b5
strict check for locale target

diff -r cf8476cc440d -r f2e70a0636b9 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Feb 02 13:56:23 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Feb 02 13:56:23 2009 +0100
@@ -316,9 +316,9 @@
 local
 
 fun init_target _ NONE = global_target
-  | init_target thy (SOME target) =
-      make_target target (Locale.defined thy (Locale.intern thy target))
-      (Class_Target.is_class thy target) ([], [], []) [];
+  | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target)
+      then make_target target true (Class_Target.is_class thy target) ([], [], []) []
+      else error ("No such locale: " ^ quote target);
 
 fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation