# HG changeset patch
# User haftmann
# Date 1228460693 -3600
# Node ID 694227dd3e8ca7a5e73030235f9df1c09c32be73
# Parent  71a7f76b522d8014156add25e55c9ace09b9c2f4
dropped NameSpace.declare_base

diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/General/name_space.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -33,7 +33,6 @@
   val default_naming: naming
   val declare: naming -> Binding.T -> T -> string * T
   val full_name: naming -> Binding.T -> string
-  val declare_base: naming -> string -> T -> T
   val external_names: naming -> string -> string list
   val path_of: naming -> string
   val add_path: string -> naming -> naming
@@ -45,6 +44,8 @@
   val bind: naming -> Binding.T * 'a
     -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+  val join_tables: (string -> 'a * 'a -> 'a)
+    -> 'a table * 'a table -> 'a table
   val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
   val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
@@ -264,13 +265,9 @@
 
 (* declarations *)
 
-fun full (Naming (path, (qualify, _))) = qualify path;
+fun full_internal (Naming (path, (qualify, _))) = qualify path;
 
-fun full_name naming b =
-  let val (prefix, bname) = Binding.dest b
-  in full (apply_prefix prefix naming) bname end;
-
-fun declare_base naming name space =
+fun declare_internal naming name space =
   if is_hidden name then
     error ("Attempt to declare hidden name " ^ quote name)
   else
@@ -282,12 +279,16 @@
       val (accs, accs') = pairself (map implode_name) (accesses naming names);
     in space |> fold (add_name name) accs |> put_accesses name accs' end;
 
+fun full_name naming b =
+  let val (prefix, bname) = Binding.dest b
+  in full_internal (apply_prefix prefix naming) bname end;
+
 fun declare bnaming b =
   let
     val (prefix, bname) = Binding.dest b;
     val naming = apply_prefix prefix bnaming;
-    val name = full naming bname;
-  in declare_base naming name #> pair name end;
+    val name = full_internal naming bname;
+  in declare_internal naming name #> pair name end;
 
 
 
@@ -303,12 +304,15 @@
   in (name, (space', Symtab.update_new (name, x) tab)) end;
 
 fun extend_table naming bentries (space, tab) =
-  let val entries = map (apfst (full naming)) bentries
-  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
+  let val entries = map (apfst (full_internal naming)) bentries
+  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
 
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.merge eq (tab1, tab2));
 
+fun join_tables f ((space1, tab1), (space2, tab2)) =
+  (merge (space1, space2), Symtab.join f (tab1, tab2));
+
 fun ext_table (space, tab) =
   Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
   |> Library.sort_wrt (#2 o #1);
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -772,7 +772,7 @@
     val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
 
     val loc_ctxt = thy' |>
-      NewLocale.register_locale name (extraTs, params)
+      NewLocale.register_locale bname (extraTs, params)
         (asm, map prop_of defs) ([], [])
         (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
       NewLocale.init name
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/Isar/local_theory.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -19,7 +19,7 @@
   val raw_theory: (theory -> theory) -> local_theory -> local_theory
   val checkpoint: local_theory -> local_theory
   val full_naming: local_theory -> NameSpace.naming
-  val full_name: local_theory -> bstring -> string
+  val full_name: local_theory -> Binding.T -> string
   val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
   val theory: (theory -> theory) -> local_theory -> local_theory
   val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
@@ -142,7 +142,7 @@
   |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
   |> NameSpace.qualified_names;
 
-fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
+fun full_name naming = NameSpace.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -387,7 +387,7 @@
     (* 1st entry: locale namespace,
        2nd entry: locales of the theory *)
 
-  val empty = (NameSpace.empty, Symtab.empty);
+  val empty = NameSpace.empty_table;
   val copy = I;
   val extend = I;
 
@@ -403,8 +403,7 @@
       regs = merge_alists (op =) regs regs',
       intros = intros,
       dests = dests};
-  fun merge _ ((space1, locs1), (space2, locs2)) =
-    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
+  fun merge _ = NameSpace.join_tables join_locales;
 );
 
 
@@ -431,10 +430,9 @@
  of SOME loc => loc
   | NONE => error ("Unknown locale " ^ quote name);
 
-fun register_locale name loc thy =
-  thy |> LocalesData.map (fn (space, locs) =>
-    (NameSpace.declare_base (Sign.naming_of thy) name space,
-      Symtab.update (name, loc) locs));
+fun register_locale bname loc thy =
+  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
+    (Binding.name bname, loc) #> snd);
 
 fun change_locale name f thy =
   let
@@ -1990,7 +1988,7 @@
       |> Sign.no_base_names
       |> PureThy.note_thmss Thm.assumptionK facts' |> snd
       |> Sign.restore_naming thy'
-      |> register_locale name {axiom = axs',
+      |> register_locale bname {axiom = axs',
         elems = map (fn e => (e, stamp ())) elems'',
         params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
         decls = ([], []),
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -10,7 +10,7 @@
 
   val clear_idents: Proof.context -> Proof.context
   val test_locale: theory -> string -> bool
-  val register_locale: string ->
+  val register_locale: bstring ->
     (string * sort) list * (Binding.T * typ option * mixfix) list ->
     term option * term list ->
     (declaration * stamp) list * (declaration * stamp) list ->
@@ -104,7 +104,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;
 
@@ -120,8 +120,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;
@@ -136,11 +135,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) =>
-    (NameSpace.declare_base (Sign.naming_of 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
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -163,11 +163,9 @@
 fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
-    val full = LocalTheory.full_name lthy;
-
     val facts' = facts
-      |> map (fn (a, bs) =>
-        (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
+      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
+          (LocalTheory.full_name lthy (fst a))) bs))
       |> PureThy.map_facts (import_export_proof lthy);
     val local_facts = PureThy.map_facts #1 facts'
       |> Attrib.map_facts (Attrib.attribute_i thy);
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/simplifier.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -177,9 +177,10 @@
 
 fun gen_simproc prep {name, lhss, proc, identifier} lthy =
   let
+    val b = Binding.name name;
     val naming = LocalTheory.full_naming lthy;
     val simproc = make_simproc
-      {name = LocalTheory.full_name lthy name,
+      {name = LocalTheory.full_name lthy b,
        lhss =
         let
           val lhss' = prep lthy lhss;
@@ -194,7 +195,7 @@
   in
     lthy |> LocalTheory.declaration (fn phi =>
       let
-        val b' = Morphism.binding phi (Binding.name name);
+        val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
       in
         Simprocs.map (fn simprocs =>
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/thm.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -1734,7 +1734,7 @@
     val naming = Sign.naming_of thy;
     val name = NameSpace.full_name naming (Binding.name bname);
     val thy' = thy |> Oracles.map (fn (space, tab) =>
-      (NameSpace.declare_base naming name space,
+      (NameSpace.declare naming (Binding.name bname) space |> snd,
         Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 
diff -r 71a7f76b522d -r 694227dd3e8c src/Pure/type.ML
--- a/src/Pure/type.ML	Thu Dec 04 14:44:07 2008 +0100
+++ b/src/Pure/type.ML	Fri Dec 05 08:04:53 2008 +0100
@@ -509,10 +509,9 @@
 fun add_class pp naming (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
-      val c' = NameSpace.full_name naming (Binding.name c);
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
-      val space' = space |> NameSpace.declare_base naming c';
+      val (c', space') = space |> NameSpace.declare naming (Binding.name c);
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
@@ -568,8 +567,7 @@
 fun new_decl naming tags (c, decl) (space, types) =
   let
     val tags' = tags |> Position.default_properties (Position.thread_data ());
-    val c' = NameSpace.full_name naming (Binding.name c);
-    val space' = NameSpace.declare_base naming c' space;
+    val (c', space') = NameSpace.declare naming (Binding.name c) space;
     val types' =
       (case Symtab.lookup types c' of
         SOME ((decl', _), _) => err_in_decls c' decl decl'