# HG changeset patch
# User haftmann
# Date 1228549538 -3600
# Node ID d808238131e7617dfdb1ed8c64de5ae309b83e3e
# Parent  01918abaa9e7690900167826552b1eb7daaaa44d# Parent  abe0f11cfa4ef96d49e2bc4d97235582df0236f0
merged

diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -230,7 +230,7 @@
 fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
   let
     val (raw_eqns, atts) = split_list eqns_atts;
-    val eqns = map (apfst Name.name_of) raw_eqns;
+    val eqns = map (apfst Binding.base_name) raw_eqns;
     val dt_info = NominalPackage.get_nominal_datatypes thy;
     val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/ROOT.ML
--- a/src/HOL/ROOT.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/ROOT.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -3,7 +3,7 @@
 Classical Higher-order Logic -- batteries included.
 *)
 
-use_thy "Complex/Complex_Main";
+use_thy "Complex_Main";
 
 val HOL_proofs = ! Proofterm.proofs;
 
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -82,7 +82,7 @@
                                       psimps, pinducts, termination, defname}) phi =
     let
       val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
-      val name = Name.name_of o Morphism.binding phi o Binding.name
+      val name = Binding.base_name o Morphism.binding phi o Binding.name
     in
       FundefCtxData { add_simps = add_simps, case_names = case_names,
                       fs = map term fs, R = term R, psimps = fact psimps, 
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -96,8 +96,8 @@
 fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
     let
       val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
-      val fixes = map (apfst (apfst Name.name_of)) fixes0;
-      val spec = map (apfst (apfst Name.name_of)) spec0;
+      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
+      val spec = map (apfst (apfst Binding.base_name)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -260,7 +260,7 @@
 
 fun check_rule ctxt cs params ((binding, att), rule) =
   let
-    val name = Name.name_of binding;
+    val err_name = Binding.display binding;
     val params' = Term.variant_frees rule (Logic.strip_params rule);
     val frees = rev (map Free params');
     val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
@@ -278,7 +278,7 @@
 
     fun check_prem' prem t =
       if head_of t mem cs then
-        check_ind (err_in_prem ctxt name rule prem) t
+        check_ind (err_in_prem ctxt err_name rule prem) t
       else (case t of
           Abs (_, _, t) => check_prem' prem t
         | t $ u => (check_prem' prem t; check_prem' prem u)
@@ -286,15 +286,15 @@
 
     fun check_prem (prem, aprem) =
       if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
-      else err_in_prem ctxt name rule prem "Non-atomic premise";
+      else err_in_prem ctxt err_name rule prem "Non-atomic premise";
   in
     (case concl of
        Const ("Trueprop", _) $ t =>
          if head_of t mem cs then
-           (check_ind (err_in_rule ctxt name rule') t;
+           (check_ind (err_in_rule ctxt err_name rule') t;
             List.app check_prem (prems ~~ aprems))
-         else err_in_rule ctxt name rule' bad_concl
-     | _ => err_in_rule ctxt name rule' bad_concl);
+         else err_in_rule ctxt err_name rule' bad_concl
+     | _ => err_in_rule ctxt err_name rule' bad_concl);
     ((binding, att), arule)
   end;
 
@@ -638,7 +638,7 @@
 
     val rec_name =
       if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
       else alt_name;
 
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
@@ -671,9 +671,9 @@
 fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
       elims raw_induct ctxt =
   let
-    val rec_name = Name.name_of rec_binding;
+    val rec_name = Binding.base_name rec_binding;
     val rec_qualified = Binding.qualify rec_name;
-    val intr_names = map Name.name_of intr_bindings;
+    val intr_names = map Binding.base_name intr_bindings;
     val ind_case_names = RuleCases.case_names intr_names;
     val induct =
       if coind then
@@ -730,11 +730,11 @@
     cs intros monos params cnames_syn ctxt =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
-    val names = map (Name.name_of o fst) cnames_syn;
+    val names = map (Binding.base_name o fst) cnames_syn;
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
-    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
     val ((intr_names, intr_atts), intr_ts) =
       apfst split_list (split_list (map (check_rule ctxt cs params) intros));
 
@@ -745,7 +745,7 @@
     val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
       params intr_ts rec_preds_defs ctxt1;
     val elims = if no_elim then [] else
-      prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
+      prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
         unfold rec_preds_defs ctxt1;
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl else
@@ -789,16 +789,16 @@
 
     (* abbrevs *)
 
-    val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
+    val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
 
     fun get_abbrev ((name, atts), t) =
       if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
         let
-          val _ = Name.name_of name = "" andalso null atts orelse
+          val _ = Binding.is_empty name andalso null atts orelse
             error "Abbreviations may not have names or attributes";
           val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
           val var =
-            (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
+            (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
               NONE => error ("Undeclared head of abbreviation " ^ quote x)
             | SOME ((b, T'), mx) =>
                 if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
@@ -807,17 +807,17 @@
       else NONE;
 
     val abbrevs = map_filter get_abbrev spec;
-    val bs = map (Name.name_of o fst o fst) abbrevs;
+    val bs = map (Binding.base_name o fst o fst) abbrevs;
 
 
     (* predicates *)
 
     val pre_intros = filter_out (is_some o get_abbrev) spec;
-    val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
-    val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
+    val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
+    val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
     val ps = map Free pnames;
 
-    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
+    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
     val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
     val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
     val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
@@ -849,7 +849,7 @@
   in
     lthy
     |> LocalTheory.set_group (serial_string ())
-    |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
+    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
   end;
 
 val add_inductive_i = gen_add_inductive_i add_ind_def;
@@ -857,7 +857,7 @@
 
 fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
   let
-    val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
+    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
       |> TheoryTarget.init NONE
       |> LocalTheory.set_group group
@@ -945,11 +945,11 @@
 fun flatten_specification specs = specs |> maps
   (fn (a, (concl, [])) => concl |> map
         (fn ((b, atts), [B]) =>
-              if Name.name_of a = "" then ((b, atts), B)
-              else if Name.name_of b = "" then ((a, atts), B)
+              if Binding.is_empty a then ((b, atts), B)
+              else if Binding.is_empty b then ((a, atts), B)
               else error "Illegal nested case names"
           | ((b, _), _) => error "Illegal simultaneous specification")
-    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
+    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
 
 fun gen_ind_decl mk_def coind =
   P.fixes -- P.for_fixes --
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -499,9 +499,9 @@
     (* convert theorems to set notation *)
     val rec_name =
       if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
+        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
       else alt_name;
-    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
+    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);
     val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
     val (intrs', elims', induct, ctxt4) =
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -194,7 +194,7 @@
     val def_name = Thm.def_name (Sign.base_name fname);
     val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     val SOME var = get_first (fn ((b, _), mx) =>
-      if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
+      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
   in (var, ((Binding.name def_name, []), rhs)) end;
 
 
@@ -231,7 +231,7 @@
   let
     val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
     val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
-      orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
+      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
     val tnames = distinct (op =) (map (#1 o snd) eqns);
     val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
     val main_fns = map (fn (tname, {index, ...}) =>
@@ -298,7 +298,7 @@
       P.name >> pair false) --| P.$$$ ")")) (false, "");
 
 val old_primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
+  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
 
 fun pipe_error t = P.!!! (Scan.fail_with (K
   (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -299,7 +299,7 @@
 
 val recdef_decl =
   Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
-  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     -- Scan.option hints
   >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
 
@@ -320,7 +320,7 @@
 val _ =
   OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
     K.thy_goal
-    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
+    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
         Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -346,19 +346,14 @@
 val get_updates = Symtab.lookup o #updates o get_sel_upd;
 fun get_simpset thy = Simplifier.theory_context thy (#simpset (get_sel_upd thy));
 
-fun put_sel_upd names simps thy =
-  let
-    val sels = map (rpair ()) names;
-    val upds = map (suffix updateN) names ~~ names;
-
-    val {records, sel_upd = {selectors, updates, simpset},
-      equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy;
-    val data = make_record_data records
-      {selectors = Symtab.extend (selectors, sels),
-        updates = Symtab.extend (updates, upds),
-        simpset = Simplifier.addsimps (simpset, simps)}
-       equalities extinjects extsplit splits extfields fieldext;
-  in RecordsData.put data thy end;
+fun put_sel_upd names simps = RecordsData.map (fn {records,
+  sel_upd = {selectors, updates, simpset},
+    equalities, extinjects, extsplit, splits, extfields, fieldext} =>
+  make_record_data records
+    {selectors = fold (fn name => Symtab.update (name, ())) names selectors,
+      updates = fold (fn name => Symtab.update ((suffix updateN) name, name)) names updates,
+      simpset = Simplifier.addsimps (simpset, simps)}
+      equalities extinjects extsplit splits extfields fieldext);
 
 
 (* access 'equalities' *)
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/refute.ML
--- a/src/HOL/Tools/refute.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/refute.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -313,18 +313,10 @@
 
   (* (string * string) -> theory -> theory *)
 
-  fun set_default_param (name, value) thy =
-  let
-    val {interpreters, printers, parameters} = RefuteData.get thy
-  in
-    RefuteData.put (case Symtab.lookup parameters name of
-      NONE   =>
+  fun set_default_param (name, value) = RefuteData.map 
+    (fn {interpreters, printers, parameters} =>
       {interpreters = interpreters, printers = printers,
-        parameters = Symtab.extend (parameters, [(name, value)])}
-    | SOME _ =>
-      {interpreters = interpreters, printers = printers,
-        parameters = Symtab.update (name, value) parameters}) thy
-  end;
+        parameters = Symtab.update (name, value) parameters});
 
 (* ------------------------------------------------------------------------- *)
 (* get_default_param: retrieves the value associated with 'name' from        *)
diff -r 01918abaa9e7 -r d808238131e7 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -233,7 +233,7 @@
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
+          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
 
 val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -244,7 +244,7 @@
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
+           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
 
 val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
diff -r 01918abaa9e7 -r d808238131e7 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -226,7 +226,7 @@
     val lengths = map length blocks;
     
     val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
-    val names = map Name.name_of bindings;
+    val names = map Binding.base_name bindings;
     val atts = map (map (prep_attrib thy)) srcss;
     val eqn_ts = map (prep_prop thy) strings;
     val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
@@ -278,7 +278,7 @@
     val ts = map (prep_term thy) strings;
     val simps = map (fix_pat thy) ts;
   in
-    (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
+    (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy
   end;
 
 val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/General/binding.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -23,6 +23,7 @@
   val add_prefix: bool -> string -> T -> T
   val map_prefix: ((string * bool) list -> T -> T) -> T -> T
   val is_empty: T -> bool
+  val base_name: T -> string
   val pos_of: T -> Position.T
   val dest: T -> (string * bool) list * string
   val display: T -> string
@@ -56,7 +57,7 @@
   else path ^ "." ^ name;
 
 val qualify = map_base o qualify_base;
-  (*FIXME should all operations on bare names moved here from name_space.ML ?*)
+  (*FIXME should all operations on bare names move here from name_space.ML ?*)
 
 fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
   else (map_binding o apfst) (cons (prfx, sticky)) b;
@@ -65,6 +66,7 @@
   f prefix (name_pos (name, pos));
 
 fun is_empty (Binding ((_, name), _)) = name = "";
+fun base_name (Binding ((_, name), _)) = name;
 fun pos_of (Binding (_, pos)) = pos;
 fun dest (Binding (prefix_name, _)) = prefix_name;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/General/name_space.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -48,7 +48,6 @@
     -> '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
 end;
 
 structure NameSpace: NAME_SPACE =
@@ -303,10 +302,6 @@
     val (name, space') = declare naming b space;
   in (name, (space', Symtab.update_new (name, x) tab)) end;
 
-fun extend_table naming bentries (space, tab) =
-  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));
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/General/table.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -41,7 +41,6 @@
   val map_entry: key -> ('a -> 'a) -> 'a table -> 'a table
   val map_default: (key * 'a) -> ('a -> 'a) -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
-  val extend: 'a table * (key * 'a) list -> 'a table                   (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a table * 'a table -> 'a table                                    (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
@@ -364,9 +363,7 @@
 
 (* simultaneous modifications *)
 
-fun extend (table, args) = fold update_new args table;
-
-fun make entries = extend (empty, entries);
+fun make entries = fold update_new entries empty;
 
 fun join f (table1, table2) =
   let fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/attrib.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -146,8 +146,8 @@
 fun add_attributes raw_attrs thy =
   let
     val new_attrs =
-      raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
-    fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
+      raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
+    fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
       handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
   in Attributes.map add thy end;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/class.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -545,7 +545,7 @@
     val constrain = Element.Constrains ((map o apsnd o map_atyps)
       (K (TFree (Name.aT, base_sort))) supparams);
     fun fork_syn (Element.Fixes xs) =
-          fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
+          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
       | fork_syn x = pair x;
     fun fork_syntax elems =
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/constdefs.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -38,7 +38,7 @@
     val prop = prep_prop var_ctxt raw_prop;
     val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
     val _ =
-      (case Option.map Name.name_of d of
+      (case Option.map Binding.base_name d of
         NONE => ()
       | SOME c' =>
           if c <> c' then
@@ -46,7 +46,7 @@
           else ());
 
     val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
-    val name = Thm.def_name_optional c (Name.name_of raw_name);
+    val name = Thm.def_name_optional c (Binding.base_name raw_name);
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/element.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -113,7 +113,7 @@
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
        let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-       let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
+       let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -136,7 +136,7 @@
 (* logical content *)
 
 fun params_of (Fixes fixes) = fixes |> map
-    (fn (x, SOME T, _) => (Name.name_of x, T)
+    (fn (x, SOME T, _) => (Binding.base_name x, T)
       | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
   | params_of _ = [];
 
@@ -182,8 +182,8 @@
       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T) = Pretty.block
-          [Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
-      | prt_var (x, NONE) = Pretty.str (Name.name_of x);
+          [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
+      | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
     val prt_vars = separate (Pretty.keyword "and") o map prt_var;
 
     fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
@@ -207,9 +207,9 @@
     fun prt_mixfix NoSyn = []
       | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
 
-    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Name.name_of x ^ " ::") ::
+    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
-      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
+      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
           Pretty.brk 1 :: prt_mixfix mx);
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
@@ -395,7 +395,7 @@
 
 fun rename_var ren (b, mx) =
   let
-    val x = Name.name_of b;
+    val x = Binding.base_name b;
     val (x', mx') = rename_var_name ren (x, mx);
   in (Binding.name x', mx') end;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -134,8 +134,8 @@
         if null dups then () else error (message ^ commas dups)
       end;
 
-    fun match_bind (n, b) = (n = Name.name_of b);
-    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
+    fun match_bind (n, b) = (n = Binding.base_name b);
+    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
       (* FIXME: cannot compare bindings for equality. *)
 
     fun params_loc loc =
@@ -177,8 +177,8 @@
 
     val (implicit, expr') = params_expr expr;
 
-    val implicit' = map (#1 #> Name.name_of) implicit;
-    val fixed' = map (#1 #> Name.name_of) fixed;
+    val implicit' = map (#1 #> Binding.base_name) implicit;
+    val fixed' = map (#1 #> Binding.base_name) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' = if strict then []
       else let val _ = reject_dups
@@ -385,7 +385,7 @@
       end;
 
 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
-      let val x = Name.name_of binding
+      let val x = Binding.base_name binding
       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   | finish_primitive _ _ (Constrains _) = Constrains []
   | finish_primitive _ close (Assumes asms) = close (Assumes asms)
@@ -396,7 +396,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = NewLocale.params_of thy loc |>
-      map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
+      map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
     val (asm, defs) = NewLocale.specification_of thy loc;
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
     val asm' = Option.map (Morphism.term morph) asm;
@@ -440,7 +440,7 @@
     fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = NewLocale.params_of thy loc |>
-          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
+          map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
         val inst' = parse_inst parm_names inst ctxt;
         val parm_types' = map (TypeInfer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -473,7 +473,7 @@
     val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
 
     (* Retrieve parameter types *)
-    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
       _ => fn ps => ps) (Fixes fors :: elems) [];
     val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
     val parms = xs ~~ Ts;  (* params from expression and elements *)
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -167,7 +167,7 @@
 (* axioms *)
 
 fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
 
 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -413,7 +413,7 @@
       opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
         >> (fn ((name, expr), insts) => Toplevel.print o
             Toplevel.theory_to_proof
-              (Locale.interpretation_cmd (Name.name_of name) expr insts)));
+              (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
 
 val _ =
   OuterSyntax.command "interpret"
@@ -422,7 +422,7 @@
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
       >> (fn ((name, expr), insts) => Toplevel.print o
           Toplevel.proof'
-            (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
+            (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
 
 
 (* classes *)
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -91,7 +91,7 @@
   let
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Name.name_of bvars;
+    val xs = map Binding.base_name bvars;
     val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -646,7 +646,7 @@
       | unify _ env = env;
     val (unifier, _) = fold unify (Ts' ~~ Us') (Vartab.empty, maxidx'');
     val Vs = map (Option.map (Envir.norm_type unifier)) Us';
-    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
+    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map_filter I Vs)) unifier;
   in map (Option.map (Envir.norm_type unifier')) Vs end;
 
 fun params_of elemss =
@@ -711,7 +711,7 @@
       (Vartab.empty, maxidx);
 
     val parms' = map (apsnd (Envir.norm_type unifier)) (distinct (eq_fst (op =)) parms);
-    val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map #2 parms'));
+    val unifier' = fold Vartab.update_new (frozen_tvars ctxt (map #2 parms')) unifier;
 
     fun inst_parms (i, ps) =
       List.foldr Term.add_typ_tfrees [] (map_filter snd ps)
@@ -1100,15 +1100,15 @@
 *)
 
 fun flatten (ctxt, _) ((ids, syn), Elem (Fixes fixes)) = let
-        val ids' = ids @ [(("", map (Name.name_of o #1) fixes), ([], Assumed []))]
+        val ids' = ids @ [(("", map (Binding.base_name o #1) fixes), ([], Assumed []))]
       in
         ((ids',
          merge_syntax ctxt ids'
-           (syn, Symtab.make (map (fn fx => (Name.name_of (#1 fx), #3 fx)) fixes))
+           (syn, Symtab.make (map (fn fx => (Binding.base_name (#1 fx), #3 fx)) fixes))
            handle Symtab.DUP x => err_in_locale ctxt
              ("Conflicting syntax for parameter: " ^ quote x)
              (map #1 ids')),
-         [((("", map (rpair NONE o Name.name_of o #1) fixes), Assumed []), Ext (Fixes fixes))])
+         [((("", map (rpair NONE o Binding.base_name o #1) fixes), Assumed []), Ext (Fixes fixes))])
       end
   | flatten _ ((ids, syn), Elem elem) =
       ((ids @ [(("", []), ([], Assumed []))], syn), [((("", []), Assumed []), Ext elem)])
@@ -1252,7 +1252,7 @@
 
 
 fun finish_ext_elem parms _ (Fixes fixes, _) = Fixes (map (fn (b, _, mx) =>
-      let val x = Name.name_of b
+      let val x = Binding.base_name b
       in (b, AList.lookup (op =) parms x, mx) end) fixes)
   | finish_ext_elem parms _ (Constrains _, _) = Constrains []
   | finish_ext_elem _ close (Assumes asms, propp) =
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/method.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -448,9 +448,9 @@
 fun add_methods raw_meths thy =
   let
     val new_meths = raw_meths |> map (fn (name, f, comment) =>
-      (name, ((f, comment), stamp ())));
+      (Binding.name name, ((f, comment), stamp ())));
 
-    fun add meths = NameSpace.extend_table (Sign.naming_of thy) new_meths meths
+    fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
       handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
   in Methods.map add thy end;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -175,7 +175,7 @@
 
 fun instance_of thy name morph =
   params_of thy name |>
-    map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
+    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
 
 fun specification_of thy name =
   let
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/obtain.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -122,7 +122,7 @@
     (*obtain vars*)
     val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
     val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
-    val xs = map (Name.name_of o #1) vars;
+    val xs = map (Binding.base_name o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -261,7 +261,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Name.name_of binding;
+    val x = Binding.base_name binding;
     val (T, ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -1012,7 +1012,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     let
-      val raw_x = Name.name_of raw_b;
+      val raw_x = Binding.base_name raw_b;
       val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
       val _ = Syntax.is_identifier (no_skolem internal x) orelse
         error ("Illegal variable name: " ^ quote x);
@@ -1122,7 +1122,7 @@
 fun gen_fixes prep raw_vars ctxt =
   let
     val (vars, _) = prep raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
+    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -153,7 +153,7 @@
 fun gen_axioms do_print prep raw_vars raw_specs thy =
   let
     val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
-    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -161,7 +161,7 @@
 
     (*axioms*)
     val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
+        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
     val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
@@ -187,7 +187,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Name.name_of b;
+            val y = Binding.base_name b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -220,7 +220,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Name.name_of b;
+            val y = Binding.base_name b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -281,11 +281,11 @@
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
-          let val name = Name.name_of b
+          let val name = Binding.base_name b
           in if name = "" then string_of_int (i + 1) else name end);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -295,7 +295,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Name.name_of bs;
+            val xs = map Binding.base_name bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -200,7 +200,7 @@
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val (prefix', _) = Binding.dest b';
-    val class_global = Name.name_of b = Name.name_of b'
+    val class_global = Binding.base_name b = Binding.base_name b'
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   in
@@ -219,7 +219,7 @@
 
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Name.name_of b;
+    val c = Binding.base_name b;
     val tags = LocalTheory.group_position_of lthy;
     val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
     val U = map #2 xs ---> T;
@@ -252,7 +252,7 @@
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
-    val c = Name.name_of b;
+    val c = Binding.base_name b;
     val tags = LocalTheory.group_position_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
@@ -289,7 +289,7 @@
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    val c = Name.name_of b;
+    val c = Binding.base_name b;
     val name' = Binding.map_base (Thm.def_name_optional c) name;
     val (rhs', rhs_conv) =
       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
@@ -310,7 +310,7 @@
           then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
           else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
     val (global_def, lthy3) = lthy2
-      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
+      |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -173,7 +173,7 @@
 
 fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
 
-fun update_trtab name trfuns tab = Symtab.extend (remove_trtab trfuns tab, trfuns)
+fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   handle Symtab.DUP c => err_dup_trfun name c;
 
 fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/Tools/invoke.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -120,7 +120,7 @@
     (K.tag_proof K.prf_goal)
     (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
       >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
-          Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
+          Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
 
 end;
 
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/name.ML
--- a/src/Pure/name.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/name.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -27,8 +27,6 @@
   val variants: string list -> context -> string list * context
   val variant_list: string list -> string list -> string list
   val variant: string list -> string -> string
-
-  val name_of: Binding.T -> string (*FIMXE legacy*)
 end;
 
 structure Name: NAME =
@@ -140,9 +138,4 @@
 fun variant_list used names = #1 (make_context used |> variants names);
 fun variant used = singleton (variant_list used);
 
-
-(** generic name bindings -- legacy **)
-
-val name_of = snd o Binding.dest;
-
 end;
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/sign.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -508,10 +508,10 @@
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     fun prep (raw_b, raw_T, raw_mx) =
       let
-        val (mx_name, mx) = Syntax.const_mixfix (Name.name_of raw_b) raw_mx;
+        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
         val b = Binding.map_base (K mx_name) raw_b;
         val c = full_name thy b;
-        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
+        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
         val T' = Logic.varifyT T;
diff -r 01918abaa9e7 -r d808238131e7 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/Pure/theory.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -178,8 +178,8 @@
 
 fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
   let
-    val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
-    val axioms' = NameSpace.extend_table (Sign.naming_of thy) axms axioms
+    val axms = map (apfst Binding.name o apsnd Logic.varify o prep_axm thy) raw_axms;
+    val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
       handle Symtab.DUP dup => err_dup_axm dup;
   in axioms' end);
 
diff -r 01918abaa9e7 -r d808238131e7 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -67,7 +67,7 @@
   val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
   val ctxt = ProofContext.init thy;
 
-  val intr_specs = map (apfst (apfst Name.name_of)) raw_intr_specs;
+  val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
   val (intr_names, intr_tms) = split_list (map fst intr_specs);
   val case_names = RuleCases.case_names intr_names;
 
diff -r 01918abaa9e7 -r d808238131e7 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Fri Dec 05 20:38:40 2008 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Sat Dec 06 08:45:38 2008 +0100
@@ -180,7 +180,7 @@
 
     val (eqn_thms', thy2) =
       thy1
-      |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
+      |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
     val (_, thy3) =
       thy2
       |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]