# HG changeset patch
# User wenzelm
# Date 1117533199 -7200
# Node ID 927627fafca5def911373b2566c2e3afaa0fdb49
# Parent  549fff1d0fc69317137bfdd79ed1481c294960ad
Sign.declare_name replaces NameSpace.extend;
tuned;

diff -r 549fff1d0fc6 -r 927627fafca5 src/Pure/goals.ML
--- a/src/Pure/goals.ML	Tue May 31 11:53:18 2005 +0200
+++ b/src/Pure/goals.ML	Tue May 31 11:53:19 2005 +0200
@@ -198,10 +198,8 @@
 
   fun print sg {space, locales, scope} =
     let
-      fun extrn name =
-        if ! long_names then name else NameSpace.extern space name;
-      val locs = map (apfst extrn) (Symtab.dest locales);
-      val scope_names = rev (map (extrn o fst) (! scope));
+      val locs = NameSpace.extern_table space locales;
+      val scope_names = rev (map (NameSpace.extern space o fst) (! scope));
     in
       [Display.pretty_name_space ("locale name space", space),
         Pretty.big_list "locales:" (map (pretty_locale sg) locs),
@@ -225,7 +223,7 @@
 fun put_locale (name, locale) thy =
   let
     val {space, locales, scope} = LocalesData.get thy;
-    val space' = NameSpace.extend (space, [name]);
+    val space' = Sign.declare_name (Theory.sign_of thy) name space;
     val locales' = Symtab.update ((name, locale), locales);
   in thy |> LocalesData.put (make_locale_data space' locales' scope) end;