Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned siganture of locale.ML
authorhaftmann
Wed, 07 Jan 2009 22:31:37 +0100
changeset 29393 172213e44992
parent 29392 aa3a30b625d1
child 29394 4638ab6c878f
tuned siganture of locale.ML
src/Pure/Isar/theory_target.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle