src/Pure/Isar/theory_target.ML
changeset 29710 f2e70a0636b9
parent 29576 669b560fc2b9
child 29971 68331b62c873
child 30240 5b25fee0362c
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Feb 02 13:56:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Feb 02 13:56:23 2009 +0100
     1.3 @@ -316,9 +316,9 @@
     1.4  local
     1.5  
     1.6  fun init_target _ NONE = global_target
     1.7 -  | init_target thy (SOME target) =
     1.8 -      make_target target (Locale.defined thy (Locale.intern thy target))
     1.9 -      (Class_Target.is_class thy target) ([], [], []) [];
    1.10 +  | init_target thy (SOME target) = if Locale.defined thy (Locale.intern thy target)
    1.11 +      then make_target target true (Class_Target.is_class thy target) ([], [], []) []
    1.12 +      else error ("No such locale: " ^ quote target);
    1.13  
    1.14  fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
    1.15    if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation