src/Pure/goals.ML

--- a/src/Pure/goals.ML	Thu Sep 01 22:15:10 2005 +0200
+++ b/src/Pure/goals.ML	Thu Sep 01 22:15:12 2005 +0200
@@ -213,13 +213,13 @@
 
 (* access locales *)
 
-fun get_locale thy name = Symtab.lookup (#locales (LocalesData.get thy), name);
+val get_locale = Symtab.curried_lookup o #locales o LocalesData.get;
 
 fun put_locale (name, locale) thy =
   let
     val {space, locales, scope} = LocalesData.get thy;
     val space' = Sign.declare_name thy name space;
-    val locales' = Symtab.update ((name, locale), locales);
+    val locales' = Symtab.curried_update (name, locale) locales;
   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;
 
 fun lookup_locale thy xname =