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