src/Pure/Isar/theory_target.ML
changeset 29393 172213e44992
parent 29360 a5be60c3674e
child 29576 669b560fc2b9
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Jan 07 22:31:36 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Jan 07 22:31:37 2009 +0100
     1.3 @@ -334,7 +334,7 @@
     1.4  
     1.5  fun init_target _ NONE = global_target
     1.6    | init_target thy (SOME target) =
     1.7 -      make_target target (Locale.test_locale thy (Locale.intern thy target))
     1.8 +      make_target target (Locale.defined thy (Locale.intern thy target))
     1.9        true (Class_Target.is_class thy target) ([], [], []) [];
    1.10  
    1.11  fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
    1.12 @@ -384,7 +384,7 @@
    1.13  
    1.14  fun context "-" thy = init NONE thy
    1.15    | context target thy = init (SOME (locale_intern
    1.16 -      (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
    1.17 +      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
    1.18  
    1.19  fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
    1.20  fun instantiation_cmd raw_arities thy =