# HG changeset patch
# User haftmann
# Date 1231363897 -3600
# Node ID 172213e44992099dbd9493b37a7671667c05b8a0
# Parent  aa3a30b625d104086bcf6aad66863d9153e218d1
tuned siganture of locale.ML

diff -r aa3a30b625d1 -r 172213e44992 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Wed Jan 07 22:31:36 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Jan 07 22:31:37 2009 +0100
@@ -334,7 +334,7 @@
 
 fun init_target _ NONE = global_target
   | init_target thy (SOME target) =
-      make_target target (Locale.test_locale thy (Locale.intern thy target))
+      make_target target (Locale.defined thy (Locale.intern thy target))
       true (Class_Target.is_class thy target) ([], [], []) [];
 
 fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
@@ -384,7 +384,7 @@
 
 fun context "-" thy = init NONE thy
   | context target thy = init (SOME (locale_intern
-      (Locale.test_locale thy (Locale.intern thy target)) thy target)) thy;
+      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
 
 fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
 fun instantiation_cmd raw_arities thy =