1.1 --- a/src/Pure/General/name_space.ML	Thu Dec 04 14:44:07 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Dec 05 08:04:53 2008 +0100
     1.3 @@ -33,7 +33,6 @@
     1.4    val default_naming: naming
     1.5    val declare: naming -> Binding.T -> T -> string * T
     1.6    val full_name: naming -> Binding.T -> string
     1.7 -  val declare_base: naming -> string -> T -> T
     1.8    val external_names: naming -> string -> string list
     1.9    val path_of: naming -> string
    1.10    val add_path: string -> naming -> naming
    1.11 @@ -45,6 +44,8 @@
    1.12    val bind: naming -> Binding.T * 'a
    1.13      -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.14    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
    1.15 +  val join_tables: (string -> 'a * 'a -> 'a)
    1.16 +    -> 'a table * 'a table -> 'a table
    1.17    val dest_table: 'a table -> (string * 'a) list
    1.18    val extern_table: 'a table -> (xstring * 'a) list
    1.19    val extend_table: naming -> (bstring * 'a) list -> 'a table -> 'a table
    1.20 @@ -264,13 +265,9 @@
    1.21  
    1.22  (* declarations *)
    1.23  
    1.24 -fun full (Naming (path, (qualify, _))) = qualify path;
    1.25 +fun full_internal (Naming (path, (qualify, _))) = qualify path;
    1.26  
    1.27 -fun full_name naming b =
    1.28 -  let val (prefix, bname) = Binding.dest b
    1.29 -  in full (apply_prefix prefix naming) bname end;
    1.30 -
    1.31 -fun declare_base naming name space =
    1.32 +fun declare_internal naming name space =
    1.33    if is_hidden name then
    1.34      error ("Attempt to declare hidden name " ^ quote name)
    1.35    else
    1.36 @@ -282,12 +279,16 @@
    1.37        val (accs, accs') = pairself (map implode_name) (accesses naming names);
    1.38      in space |> fold (add_name name) accs |> put_accesses name accs' end;
    1.39  
    1.40 +fun full_name naming b =
    1.41 +  let val (prefix, bname) = Binding.dest b
    1.42 +  in full_internal (apply_prefix prefix naming) bname end;
    1.43 +
    1.44  fun declare bnaming b =
    1.45    let
    1.46      val (prefix, bname) = Binding.dest b;
    1.47      val naming = apply_prefix prefix bnaming;
    1.48 -    val name = full naming bname;
    1.49 -  in declare_base naming name #> pair name end;
    1.50 +    val name = full_internal naming bname;
    1.51 +  in declare_internal naming name #> pair name end;
    1.52  
    1.53  
    1.54  
    1.55 @@ -303,12 +304,15 @@
    1.56    in (name, (space', Symtab.update_new (name, x) tab)) end;
    1.57  
    1.58  fun extend_table naming bentries (space, tab) =
    1.59 -  let val entries = map (apfst (full naming)) bentries
    1.60 -  in (fold (declare_base naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.61 +  let val entries = map (apfst (full_internal naming)) bentries
    1.62 +  in (fold (declare_internal naming o #1) entries space, Symtab.extend (tab, entries)) end;
    1.63  
    1.64  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    1.65    (merge (space1, space2), Symtab.merge eq (tab1, tab2));
    1.66  
    1.67 +fun join_tables f ((space1, tab1), (space2, tab2)) =
    1.68 +  (merge (space1, space2), Symtab.join f (tab1, tab2));
    1.69 +
    1.70  fun ext_table (space, tab) =
    1.71    Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
    1.72    |> Library.sort_wrt (#2 o #1);

     2.1 --- a/src/Pure/Isar/expression.ML	Thu Dec 04 14:44:07 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 05 08:04:53 2008 +0100
     2.3 @@ -772,7 +772,7 @@
     2.4      val deps' = map (fn (l, morph) => (l, morph $> satisfy)) deps;
     2.5  
     2.6      val loc_ctxt = thy' |>
     2.7 -      NewLocale.register_locale name (extraTs, params)
     2.8 +      NewLocale.register_locale bname (extraTs, params)
     2.9          (asm, map prop_of defs) ([], [])
    2.10          (map (fn n => (n, stamp ())) notes |> rev) (map (fn d => (d, stamp ())) deps' |> rev) |>
    2.11        NewLocale.init name

     3.1 --- a/src/Pure/Isar/local_theory.ML	Thu Dec 04 14:44:07 2008 +0100
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Dec 05 08:04:53 2008 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4    val raw_theory: (theory -> theory) -> local_theory -> local_theory
     3.5    val checkpoint: local_theory -> local_theory
     3.6    val full_naming: local_theory -> NameSpace.naming
     3.7 -  val full_name: local_theory -> bstring -> string
     3.8 +  val full_name: local_theory -> Binding.T -> string
     3.9    val theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    3.10    val theory: (theory -> theory) -> local_theory -> local_theory
    3.11    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    3.12 @@ -142,7 +142,7 @@
    3.13    |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
    3.14    |> NameSpace.qualified_names;
    3.15  
    3.16 -fun full_name naming = NameSpace.full_name (full_naming naming) o Binding.name;
    3.17 +fun full_name naming = NameSpace.full_name (full_naming naming);
    3.18  
    3.19  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    3.20    |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))

     4.1 --- a/src/Pure/Isar/locale.ML	Thu Dec 04 14:44:07 2008 +0100
     4.2 +++ b/src/Pure/Isar/locale.ML	Fri Dec 05 08:04:53 2008 +0100
     4.3 @@ -387,7 +387,7 @@
     4.4      (* 1st entry: locale namespace,
     4.5         2nd entry: locales of the theory *)
     4.6  
     4.7 -  val empty = (NameSpace.empty, Symtab.empty);
     4.8 +  val empty = NameSpace.empty_table;
     4.9    val copy = I;
    4.10    val extend = I;
    4.11  
    4.12 @@ -403,8 +403,7 @@
    4.13        regs = merge_alists (op =) regs regs',
    4.14        intros = intros,
    4.15        dests = dests};
    4.16 -  fun merge _ ((space1, locs1), (space2, locs2)) =
    4.17 -    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
    4.18 +  fun merge _ = NameSpace.join_tables join_locales;
    4.19  );
    4.20  
    4.21  
    4.22 @@ -431,10 +430,9 @@
    4.23   of SOME loc => loc
    4.24    | NONE => error ("Unknown locale " ^ quote name);
    4.25  
    4.26 -fun register_locale name loc thy =
    4.27 -  thy |> LocalesData.map (fn (space, locs) =>
    4.28 -    (NameSpace.declare_base (Sign.naming_of thy) name space,
    4.29 -      Symtab.update (name, loc) locs));
    4.30 +fun register_locale bname loc thy =
    4.31 +  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy)
    4.32 +    (Binding.name bname, loc) #> snd);
    4.33  
    4.34  fun change_locale name f thy =
    4.35    let
    4.36 @@ -1990,7 +1988,7 @@
    4.37        |> Sign.no_base_names
    4.38        |> PureThy.note_thmss Thm.assumptionK facts' |> snd
    4.39        |> Sign.restore_naming thy'
    4.40 -      |> register_locale name {axiom = axs',
    4.41 +      |> register_locale bname {axiom = axs',
    4.42          elems = map (fn e => (e, stamp ())) elems'',
    4.43          params = params_of elemss''' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
    4.44          decls = ([], []),

     5.1 --- a/src/Pure/Isar/new_locale.ML	Thu Dec 04 14:44:07 2008 +0100
     5.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 08:04:53 2008 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4  
     5.5    val clear_idents: Proof.context -> Proof.context
     5.6    val test_locale: theory -> string -> bool
     5.7 -  val register_locale: string ->
     5.8 +  val register_locale: bstring ->
     5.9      (string * sort) list * (Binding.T * typ option * mixfix) list ->
    5.10      term option * term list ->
    5.11      (declaration * stamp) list * (declaration * stamp) list ->
    5.12 @@ -104,7 +104,7 @@
    5.13    type T = NameSpace.T * locale Symtab.table;
    5.14      (* locale namespace and locales of the theory *)
    5.15  
    5.16 -  val empty = (NameSpace.empty, Symtab.empty);
    5.17 +  val empty = NameSpace.empty_table;
    5.18    val copy = I;
    5.19    val extend = I;
    5.20  
    5.21 @@ -120,8 +120,7 @@
    5.22              dependencies = s_merge (dependencies, dependencies')
    5.23            }          
    5.24          end;
    5.25 -  fun merge _ ((space1, locs1), (space2, locs2)) =
    5.26 -    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
    5.27 +  fun merge _ = NameSpace.join_tables join_locales;
    5.28  );
    5.29  
    5.30  val intern = NameSpace.intern o #1 o LocalesData.get;
    5.31 @@ -136,11 +135,10 @@
    5.32  fun test_locale thy name = case get_locale thy name
    5.33   of SOME _ => true | NONE => false;
    5.34  
    5.35 -fun register_locale name parameters spec decls notes dependencies thy =
    5.36 -  thy |> LocalesData.map (fn (space, locs) =>
    5.37 -    (NameSpace.declare_base (Sign.naming_of thy) name space, Symtab.update (name,
    5.38 -      Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
    5.39 -        dependencies = dependencies}) locs));
    5.40 +fun register_locale bname parameters spec decls notes dependencies thy =
    5.41 +  thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (Binding.name bname,
    5.42 +    Loc {parameters = parameters, spec = spec, decls = decls, notes = notes,
    5.43 +      dependencies = dependencies}) #> snd);
    5.44  
    5.45  fun change_locale name f thy =
    5.46    let

     6.1 --- a/src/Pure/Isar/theory_target.ML	Thu Dec 04 14:44:07 2008 +0100
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 05 08:04:53 2008 +0100
     6.3 @@ -163,11 +163,9 @@
     6.4  fun notes (Target {target, is_locale, is_class, ...}) kind facts lthy =
     6.5    let
     6.6      val thy = ProofContext.theory_of lthy;
     6.7 -    val full = LocalTheory.full_name lthy;
     6.8 -
     6.9      val facts' = facts
    6.10 -      |> map (fn (a, bs) =>
    6.11 -        (a, PureThy.burrow_fact (PureThy.name_multi (full (Name.name_of (fst a)))) bs))
    6.12 +      |> map (fn (a, bs) => (a, PureThy.burrow_fact (PureThy.name_multi
    6.13 +          (LocalTheory.full_name lthy (fst a))) bs))
    6.14        |> PureThy.map_facts (import_export_proof lthy);
    6.15      val local_facts = PureThy.map_facts #1 facts'
    6.16        |> Attrib.map_facts (Attrib.attribute_i thy);

     7.1 --- a/src/Pure/simplifier.ML	Thu Dec 04 14:44:07 2008 +0100
     7.2 +++ b/src/Pure/simplifier.ML	Fri Dec 05 08:04:53 2008 +0100
     7.3 @@ -177,9 +177,10 @@
     7.4  
     7.5  fun gen_simproc prep {name, lhss, proc, identifier} lthy =
     7.6    let
     7.7 +    val b = Binding.name name;
     7.8      val naming = LocalTheory.full_naming lthy;
     7.9      val simproc = make_simproc
    7.10 -      {name = LocalTheory.full_name lthy name,
    7.11 +      {name = LocalTheory.full_name lthy b,
    7.12         lhss =
    7.13          let
    7.14            val lhss' = prep lthy lhss;
    7.15 @@ -194,7 +195,7 @@
    7.16    in
    7.17      lthy |> LocalTheory.declaration (fn phi =>
    7.18        let
    7.19 -        val b' = Morphism.binding phi (Binding.name name);
    7.20 +        val b' = Morphism.binding phi b;
    7.21          val simproc' = morph_simproc phi simproc;
    7.22        in
    7.23          Simprocs.map (fn simprocs =>

     8.1 --- a/src/Pure/thm.ML	Thu Dec 04 14:44:07 2008 +0100
     8.2 +++ b/src/Pure/thm.ML	Fri Dec 05 08:04:53 2008 +0100
     8.3 @@ -1734,7 +1734,7 @@
     8.4      val naming = Sign.naming_of thy;
     8.5      val name = NameSpace.full_name naming (Binding.name bname);
     8.6      val thy' = thy |> Oracles.map (fn (space, tab) =>
     8.7 -      (NameSpace.declare_base naming name space,
     8.8 +      (NameSpace.declare naming (Binding.name bname) space |> snd,
     8.9          Symtab.update_new (name, stamp ()) tab handle Symtab.DUP dup => err_dup_ora dup));
    8.10    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
    8.11  

     9.1 --- a/src/Pure/type.ML	Thu Dec 04 14:44:07 2008 +0100
     9.2 +++ b/src/Pure/type.ML	Fri Dec 05 08:04:53 2008 +0100
     9.3 @@ -509,10 +509,9 @@
     9.4  fun add_class pp naming (c, cs) tsig =
     9.5    tsig |> map_tsig (fn ((space, classes), default, types) =>
     9.6      let
     9.7 -      val c' = NameSpace.full_name naming (Binding.name c);
     9.8        val cs' = map (cert_class tsig) cs
     9.9          handle TYPE (msg, _, _) => error msg;
    9.10 -      val space' = space |> NameSpace.declare_base naming c';
    9.11 +      val (c', space') = space |> NameSpace.declare naming (Binding.name c);
    9.12        val classes' = classes |> Sorts.add_class pp (c', cs');
    9.13      in ((space', classes'), default, types) end);
    9.14  
    9.15 @@ -568,8 +567,7 @@
    9.16  fun new_decl naming tags (c, decl) (space, types) =
    9.17    let
    9.18      val tags' = tags |> Position.default_properties (Position.thread_data ());
    9.19 -    val c' = NameSpace.full_name naming (Binding.name c);
    9.20 -    val space' = NameSpace.declare_base naming c' space;
    9.21 +    val (c', space') = NameSpace.declare naming (Binding.name c) space;
    9.22      val types' =
    9.23        (case Symtab.lookup types c' of
    9.24          SOME ((decl', _), _) => err_in_decls c' decl decl'