renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
minor tuning;

--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -546,7 +546,7 @@
     Proof.theorem_i NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Sign.base_name names);
-        val rec_qualified = Binding.qualify rec_name;
+        val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = RuleCases.case_names induct_cases;
         val induct_cases' = InductivePackage.partition_rules' raw_induct
           (intrs ~~ induct_cases); 

--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -453,7 +453,7 @@
     Proof.theorem_i NONE (fn thss => fn ctxt =>
       let
         val rec_name = space_implode "_" (map Sign.base_name names);
-        val rec_qualified = Binding.qualify rec_name;
+        val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = RuleCases.case_names induct_cases;
         val induct_cases' = InductivePackage.partition_rules' raw_induct
           (intrs ~~ induct_cases); 

--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -210,7 +210,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 Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
+      if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
   in
     ((var, ((Binding.name def_name, []), rhs)),
      subst_bounds (rev (map Free frees), strip_abs_body rhs))
@@ -248,7 +248,7 @@
     val (names_atts, spec') = split_list spec;
     val eqns' = map unquantify spec'
     val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
-      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes)) spec' [];
+      orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
     val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
       map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
@@ -285,7 +285,7 @@
       set_group ? LocalTheory.set_group (serial_string ()) |>
       fold_map (apfst (snd o snd) oo
         LocalTheory.define Thm.definitionK o fst) defs';
-    val qualify = Binding.qualify
+    val qualify = Binding.qualify false
       (space_implode "_" (map (Sign.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;
     val cert = cterm_of (ProofContext.theory_of lthy');

--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 18:32:01 2009 +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 = Binding.base_name o Morphism.binding phi o Binding.name
+      val name = Binding.name_of 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, 

--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -99,8 +99,8 @@
       val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
       val ((fixes0, spec0), ctxt') = 
         prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
-      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
-      val spec = map (apfst (apfst Binding.base_name)) spec0;
+      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
+      val spec = map (apfst (apfst Binding.name_of)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes

--- a/src/HOL/Tools/inductive_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -639,7 +639,7 @@
 
     val rec_name =
       if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
+        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
 
     val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
@@ -674,9 +674,9 @@
 fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
       elims raw_induct ctxt =
   let
-    val rec_name = Binding.base_name rec_binding;
-    val rec_qualified = Binding.qualify rec_name;
-    val intr_names = map Binding.base_name intr_bindings;
+    val rec_name = Binding.name_of rec_binding;
+    val rec_qualified = Binding.qualify false rec_name;
+    val intr_names = map Binding.name_of intr_bindings;
     val ind_case_names = RuleCases.case_names intr_names;
     val induct =
       if coind then
@@ -734,7 +734,7 @@
     cs intros monos params cnames_syn ctxt =
   let
     val _ = null cnames_syn andalso error "No inductive predicates given";
-    val names = map (Binding.base_name o fst) cnames_syn;
+    val names = map (Binding.name_of o fst) cnames_syn;
     val _ = message (quiet_mode andalso not verbose)
       ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
 
@@ -749,7 +749,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 Binding.base_name intr_names)
+      prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
         unfold rec_preds_defs ctxt1;
     val raw_induct = zero_var_indexes
       (if no_ind then Drule.asm_rl else
@@ -793,7 +793,7 @@
 
     (* abbrevs *)
 
-    val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
+    val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;
 
     fun get_abbrev ((name, atts), t) =
       if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
@@ -802,7 +802,7 @@
             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, _), _) => Binding.base_name c = x) cnames_syn of
+            (case find_first (fn ((c, _), _) => Binding.name_of 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)
@@ -811,17 +811,17 @@
       else NONE;
 
     val abbrevs = map_filter get_abbrev spec;
-    val bs = map (Binding.base_name o fst o fst) abbrevs;
+    val bs = map (Binding.name_of 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 Binding.base_name o fst o fst) cnames_syn;
-    val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
+    val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn;
+    val cs = map (Free o apfst Binding.name_of o fst) cnames_syn';
     val ps = map Free pnames;
 
-    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
+    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of 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;
@@ -854,7 +854,7 @@
   in
     lthy
     |> LocalTheory.set_group (serial_string ())
-    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
+    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
   end;
 
 val add_inductive_i = gen_add_inductive_i add_ind_def;
@@ -954,7 +954,7 @@
               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 (Binding.base_name a)));
+    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
 
 fun gen_ind_decl mk_def coind =
   P.fixes -- P.for_fixes --

--- a/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -464,7 +464,7 @@
            | NONE => u)) |>
         Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
         eta_contract (member op = cs' orf is_pred pred_arities))) intros;
-    val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
+    val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
     val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
     val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
       InductivePackage.add_ind_def
@@ -501,7 +501,7 @@
     (* convert theorems to set notation *)
     val rec_name =
       if Binding.is_empty alt_name then
-        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
+        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
       else alt_name;
     val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn;  (* FIXME *)
     val (intr_names, intr_atts) = split_list (map fst intros);

--- a/src/HOL/Tools/primrec_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Tue Mar 03 18:32:01 2009 +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 Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
+      if Binding.name_of 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 = Binding.base_name w) fixes) o snd) spec [];
+      orelse exists (fn ((w, _), _) => v = Binding.name_of 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, ...}) =>
@@ -248,7 +248,7 @@
       else primrec_error ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
-    val qualify = Binding.qualify prefix;
+    val qualify = Binding.qualify false prefix;
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
     val simp_atts = map (Attrib.internal o K)
@@ -299,7 +299,7 @@
       P.name >> pair false) --| P.$$$ ")")) (false, "");
 
 val old_primrec_decl =
-  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
+  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
 
 fun pipe_error t = P.!!! (Scan.fail_with (K
   (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));

--- a/src/HOL/Tools/recdef_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -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 Binding.base_name) -- P.xname --
+    ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
         Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
       >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
 

--- a/src/HOL/Tools/specification_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -232,7 +232,7 @@
 
 val specification_decl =
   P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
+          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
 
 val _ =
   OuterSyntax.command "specification" "define constants by specification" K.thy_goal
@@ -243,7 +243,7 @@
 val ax_specification_decl =
     P.name --
     (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
-           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
+           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
 
 val _ =
   OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal

--- a/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -175,7 +175,7 @@
   (spec : (Attrib.binding * term) list)
   (lthy : local_theory) =
   let
-    val names = map (Binding.base_name o fst o fst) fixes;
+    val names = map (Binding.name_of o fst o fst) fixes;
     val all_names = space_implode "_" names;
     val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
     val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));

--- a/src/Pure/Isar/args.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -170,7 +170,7 @@
 val name_source_position = named >> T.source_position_of;
 
 val name = named >> T.content_of;
-val binding = P.position name >> Binding.name_pos;
+val binding = P.position name >> Binding.make;
 val alt_name = alt_string >> T.content_of;
 val symbol = symbolic >> T.content_of;
 val liberal_name = symbol || name;

--- a/src/Pure/Isar/class.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -201,7 +201,7 @@
       | check_element e = [()];
     val _ = map check_element syntax_elems;
     fun fork_syn (Element.Fixes xs) =
-          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
+          fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
           #>> Element.Fixes
       | fork_syn x = pair x;
     val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
@@ -228,7 +228,7 @@
     val raw_params = (snd o chop (length supparams)) all_params;
     fun add_const (b, SOME raw_ty, _) thy =
       let
-        val v = Binding.base_name b;
+        val v = Binding.name_of b;
         val c = Sign.full_bname thy v;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
         val ty0 = Type.strip_sorts ty;

--- a/src/Pure/Isar/constdefs.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -36,7 +36,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 Binding.base_name d of
+      (case Option.map Binding.name_of d of
         NONE => ()
       | SOME c' =>
           if c <> c' then
@@ -44,7 +44,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 (Binding.base_name raw_name);
+    val name = Thm.def_name_optional c (Binding.name_of raw_name);
     val atts = map (prep_att thy) raw_atts;
 
     val thy' =

--- a/src/Pure/Isar/element.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -96,7 +96,7 @@
 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-      (Binding.base_name (binding (Binding.name x)), typ T)))
+      (Binding.name_of (binding (Binding.name x)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
@@ -143,8 +143,8 @@
       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T) = Pretty.block
-          [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
-      | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
+          [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
+      | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
     val prt_vars = separate (Pretty.keyword "and") o map prt_var;
 
     fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
@@ -168,9 +168,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 (Binding.base_name x ^ " ::") ::
+    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
-      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
+      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
           Pretty.brk 1 :: prt_mixfix mx);
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
@@ -502,7 +502,7 @@
         val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
+            in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
         val (_, ctxt') =
           ctxt |> fold (Variable.auto_fixes o #1) asms
           |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
@@ -527,7 +527,7 @@
 
 fun prep_facts prep_name get intern ctxt =
   map_ctxt
-   {binding = Binding.map_base prep_name,
+   {binding = Binding.map_name prep_name,
     typ = I,
     term = I,
     pattern = I,

--- a/src/Pure/Isar/expression.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -88,10 +88,10 @@
         if null dups then () else error (message ^ commas dups)
       end;
 
-    fun match_bind (n, b) = (n = Binding.base_name b);
+    fun match_bind (n, b) = (n = Binding.name_of b);
     fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
       (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
-      Binding.base_name b1 = Binding.base_name b2 andalso
+      Binding.name_of b1 = Binding.name_of b2 andalso
         (mx1 = mx2 orelse
           error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
       
@@ -129,8 +129,8 @@
 
     val (implicit, expr') = params_expr expr;
 
-    val implicit' = map (#1 #> Binding.base_name) implicit;
-    val fixed' = map (#1 #> Binding.base_name) fixed;
+    val implicit' = map (#1 #> Binding.name_of) implicit;
+    val fixed' = map (#1 #> Binding.name_of) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' = if strict then []
       else let val _ = reject_dups
@@ -306,14 +306,12 @@
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
-            in
-              ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
-            end))
+            in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
         | e => e)
       end;
 
 fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
-      let val x = Binding.base_name binding
+      let val x = Binding.name_of binding
       in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   | finish_primitive _ _ (Constrains _) = Constrains []
   | finish_primitive _ close (Assumes asms) = close (Assumes asms)
@@ -324,7 +322,7 @@
   let
     val thy = ProofContext.theory_of ctxt;
     val (parm_names, parm_types) = Locale.params_of thy loc |>
-      map_split (fn (b, SOME T, _) => (Binding.base_name b, T));
+      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
@@ -356,7 +354,7 @@
     fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
       let
         val (parm_names, parm_types) = Locale.params_of thy loc |>
-          map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
+          map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
             (*FIXME return value of Locale.params_of has strange type*)
         val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
@@ -390,7 +388,7 @@
       prep_concl raw_concl (insts', elems, ctxt5);
 
     (* Retrieve parameter types *)
-    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes)
+    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
       | _ => fn ps => ps) (Fixes fors :: elems') [];
     val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; 
     val parms = xs ~~ Ts;  (* params from expression and elements *)

--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -161,7 +161,7 @@
 (* axioms *)
 
 fun add_axms f args thy =
-  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
+  f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
 
 val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
 

--- a/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -90,8 +90,8 @@
   let
     val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
     val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
-    val xs = map Binding.base_name bvars;
-    val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
+    val xs = map Binding.name_of bvars;
+    val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
     val eqs = mk_def ctxt (xs ~~ rhss);
     val lhss = map (fst o Logic.dest_equals) eqs;
   in

--- a/src/Pure/Isar/locale.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -194,7 +194,7 @@
 fun axioms_of thy = #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
+  map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
 
 fun specification_of thy = #spec o the_locale thy;
 
@@ -464,8 +464,7 @@
 fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
 
 fun add_decls add loc decl =
-  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
-    #>
+  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   add_thmss loc Thm.internalK
     [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
 

--- a/src/Pure/Isar/obtain.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -119,7 +119,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 (Binding.base_name o #1) vars;
+    val xs = map (Binding.name_of o #1) vars;
 
     (*obtain asms*)
     val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
@@ -258,7 +258,7 @@
 
 fun inferred_type (binding, _, mx) ctxt =
   let
-    val x = Binding.base_name binding;
+    val x = Binding.name_of binding;
     val (T, ctxt') = ProofContext.inferred_param x ctxt
   in ((x, T, mx), ctxt') end;
 

--- a/src/Pure/Isar/outer_parse.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -228,7 +228,7 @@
 (* names and text *)
 
 val name = group "name declaration" (short_ident || sym_ident || string || number);
-val binding = position name >> Binding.name_pos;
+val binding = position name >> Binding.make;
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
 val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
 val path = group "file name/path specification" name >> Path.explode;

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -1008,7 +1008,7 @@
 fun prep_vars prep_typ internal =
   fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     let
-      val raw_x = Binding.base_name raw_b;
+      val raw_x = Binding.name_of 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);
@@ -1017,7 +1017,7 @@
         if internal then T
         else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
       val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
-      val var = (Binding.map_base (K x) raw_b, opt_T, mx);
+      val var = (Binding.map_name (K x) raw_b, opt_T, mx);
     in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
 
 in
@@ -1118,7 +1118,7 @@
 fun gen_fixes prep raw_vars ctxt =
   let
     val (vars, _) = prep raw_vars ctxt;
-    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
+    val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
     val ctxt'' =
       ctxt'
       |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)

--- a/src/Pure/Isar/specification.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -140,7 +140,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), _) => (Binding.base_name b, T)) vars;
+    val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
 
     (*consts*)
     val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
@@ -148,8 +148,8 @@
 
     (*axioms*)
     val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom
-          ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
+        fold_map Thm.add_axiom  (* FIXME proper use of binding!? *)
+          ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of 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);
@@ -169,19 +169,19 @@
     val (vars, [((raw_name, atts), [prop])]) =
       fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
     val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
-    val name = Binding.map_base (Thm.def_name_optional x) raw_name;
+    val name = Binding.map_name (Thm.def_name_optional x) raw_name;
     val var =
       (case vars of
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.base_name b;
+            val y = Binding.name_of b;
             val _ = x = y orelse
               error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
           in (b, mx) end);
     val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
-        (var, ((Binding.map_base (suffix "_raw") name, []), rhs));
+        (var, ((Binding.map_name (suffix "_raw") name, []), rhs));
     val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
         ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
 
@@ -208,7 +208,7 @@
         [] => (Binding.name x, NoSyn)
       | [((b, _), mx)] =>
           let
-            val y = Binding.base_name b;
+            val y = Binding.name_of b;
             val _ = x = y orelse
               error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
                 Position.str_of (Binding.pos_of b));
@@ -269,11 +269,10 @@
   | Element.Obtains obtains =>
       let
         val case_names = obtains |> map_index (fn (i, (b, _)) =>
-          let val name = Binding.base_name b
-          in if name = "" then string_of_int (i + 1) else name end);
+          if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b);
         val constraints = obtains |> map (fn (_, (vars, _)) =>
           Element.Constrains
-            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
+            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
 
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
@@ -283,7 +282,7 @@
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
             val bs = map fst vars;
-            val xs = map Binding.base_name bs;
+            val xs = map Binding.name_of bs;
             val props = map fst asms;
             val (Ts, _) = ctxt'
               |> fold Variable.declare_term props

--- a/src/Pure/Isar/theory_target.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -188,8 +188,8 @@
     val arg = (b', Term.close_schematic_term rhs');
     val similar_body = Type.similar_types (rhs, rhs');
     (* FIXME workaround based on educated guess *)
-    val (prefix', _) = Binding.dest b';
-    val class_global = Binding.base_name b = Binding.base_name b'
+    val (prefix', _, _) = Binding.dest b';
+    val class_global = Binding.name_of b = Binding.name_of b'
       andalso not (null prefix')
       andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
   in
@@ -206,14 +206,15 @@
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
 fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   let
-    val c = Binding.base_name b;
+    val c = Binding.name_of 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;
     val (mx1, mx2, mx3) = fork_mixfix ta mx;
-    fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
     val declare_const =
       (case Class_Target.instantiation_param lthy c of
         SOME c' =>
@@ -241,7 +242,7 @@
 
 fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   let
-    val c = Binding.base_name b;
+    val c = Binding.name_of b;
     val tags = LocalTheory.group_position_of lthy;
     val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
     val target_ctxt = LocalTheory.target_of lthy;
@@ -278,8 +279,8 @@
     val thy = ProofContext.theory_of lthy;
     val thy_ctxt = ProofContext.init thy;
 
-    val c = Binding.base_name b;
-    val name' = Binding.map_base (Thm.def_name_optional c) name;
+    val c = Binding.name_of b;
+    val name' = Binding.map_name (Thm.def_name_optional c) name;
     val (rhs', rhs_conv) =
       LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
     val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
@@ -299,7 +300,7 @@
           then (fn name => fn eq => Thm.add_def false false (Binding.name 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 (Binding.base_name name') (lhs', rhs'));
+      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
     val def = LocalDefs.trans_terms lthy3
       [(*c == global.c xs*)     local_def,
        (*global.c xs == rhs'*)  global_def,

--- a/src/Pure/sign.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/Pure/sign.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -507,10 +507,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 (Binding.base_name raw_b) raw_mx;
-        val b = Binding.map_base (K mx_name) raw_b;
+        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
+        val b = Binding.map_name (K mx_name) raw_b;
         val c = full_name thy b;
-        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
+        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
           cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT T;

--- a/src/ZF/Tools/inductive_package.ML	Tue Mar 03 18:31:59 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Tue Mar 03 18:32:01 2009 +0100
@@ -65,7 +65,7 @@
   val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
   val ctxt = ProofContext.init thy;
 
-  val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
+  val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
   val (intr_names, intr_tms) = split_list (map fst intr_specs);
   val case_names = RuleCases.case_names intr_names;