src/Pure/Isar/new_locale.ML

--- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:26:07 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 11:42:27 2008 +0100
@@ -9,8 +9,8 @@
   type locale
 
   val test_locale: theory -> string -> bool
-  val register_locale: string ->
-    (string * sort) list * (Name.binding * typ option * mixfix) list ->
+  val register_locale: bstring ->
+    (string * sort) list * (Binding.T * typ option * mixfix) list ->
     term option * term list ->
     (declaration * stamp) list * (declaration * stamp) list ->
     ((string * (Attrib.binding * (thm list * Attrib.src list) list) list) * stamp) list ->
@@ -21,7 +21,7 @@
   val extern: theory -> string -> xstring
 
   (* Specification *)
-  val params_of: theory -> string -> (Name.binding * typ option * mixfix) list
+  val params_of: theory -> string -> (Binding.T * typ option * mixfix) list
   val instance_of: theory -> string -> Morphism.morphism -> term list
   val specification_of: theory -> string -> term option * term list
   val declarations_of: theory -> string -> declaration list * declaration list
@@ -91,7 +91,7 @@
 
 datatype locale = Loc of {
   (* extensible lists are in reverse order: decls, notes, dependencies *)
-  parameters: (string * sort) list * (Name.binding * typ option * mixfix) list,
+  parameters: (string * sort) list * (Binding.T * typ option * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
@@ -111,7 +111,7 @@
   type T = NameSpace.T * locale Symtab.table;
     (* locale namespace and locales of the theory *)
 
-  val empty = (NameSpace.empty, Symtab.empty);
+  val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
 
@@ -127,8 +127,7 @@
             dependencies = s_merge (dependencies, dependencies')
           }          
         end;
-  fun merge _ ((space1, locs1), (space2, locs2)) =
-    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
+  fun merge _ = NameSpace.join_tables join_locales;
 );
 
 val intern = NameSpace.intern o #1 o LocalesData.get;
@@ -143,11 +142,10 @@
 fun test_locale thy name = case get_locale thy name
  of SOME _ => true | NONE => false;
 
-fun register_locale name parameters spec decls notes dependencies thy =
-  thy |> LocalesData.map (fn (space, locs) =>
-    (Sign.declare_name thy name space, Symtab.update (name,
-      Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
-        dependencies = dependencies}) locs));
+fun register_locale bname parameters spec decls notes dependencies thy =
+  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
+    Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
+      dependencies = dependencies}) #> snd);
 
 fun change_locale name f thy =
   let
@@ -311,9 +309,9 @@
     input |>
       (if not (null params) then activ_elem (Fixes params) else I) |>
       (* FIXME type parameters *)
-      (if is_some asm then activ_elem (Assumes [(Attrib.no_binding, [(the asm, [])])]) else I) |>
+      (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
       (if not (null defs)
-        then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
+        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
         else I) |>
       pair marked |> roundup thy (activate_notes activ_elem) (name, Morphism.identity)
   end;
@@ -408,7 +406,7 @@
     (fn (parameters, spec, decls, notes, dependencies) =>
       (parameters, spec, add (decl, stamp ()) decls, notes, dependencies))) #>
   add_thmss loc Thm.internalK
-    [((Name.no_binding, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+    [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
 
 in