# HG changeset patch
# User wenzelm
# Date 1236101601 -3600
# Node ID 2bf6432b9740e76f6c71a4586e05cf9a75f0ae41
# Parent  79136ce06bdbb26d7d0940603d64fbd2716bf3e9# Parent  24d97535287997e7a380cca40e824e5d6d47953b
merged

diff -r 79136ce06bdb -r 2bf6432b9740 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Mar 03 17:05:18 2009 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Tue Mar 03 18:33:21 2009 +0100
@@ -1010,7 +1010,7 @@
      \end{picture}
      \caption{Subclass relationship of monoids and groups:
         before and after establishing the relationship
-        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges left out.}
+        \isa{group\ {\isasymsubseteq}\ monoid};  transitive edges are left out.}
      \label{fig:subclass}
    \end{center}
   \end{figure}
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 18:33:21 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); 
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 18:33:21 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); 
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 18:33:21 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');
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/function_package/fundef_common.ML
--- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 18:33:21 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, 
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 18:33:21 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
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -260,7 +260,7 @@
 
 fun check_rule ctxt cs params ((binding, att), rule) =
   let
-    val err_name = Binding.display binding;
+    val err_name = Binding.str_of 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);
@@ -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 --
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 18:33:21 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);
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Tue Mar 03 18:33:21 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])));
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Tue Mar 03 18:33:21 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));
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Mar 03 18:33:21 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
diff -r 79136ce06bdb -r 2bf6432b9740 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -16,7 +16,7 @@
     -> (Attrib.binding * term) list -> local_theory -> local_theory
 
   val add_fixpat: Attrib.binding * string list -> theory -> theory
-  val add_fixpat_i: (binding * attribute list) * term list -> theory -> theory
+  val add_fixpat_i: Thm.binding * term list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
   val setup: theory -> theory
 end;
@@ -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));
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/binding.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -1,98 +1,99 @@
 (*  Title:      Pure/General/binding.ML
     Author:     Florian Haftmann, TU Muenchen
+    Author:     Makarius
 
 Structured name bindings.
 *)
 
-signature BASIC_BINDING =
-sig
-  type binding
-  val long_names: bool ref
-  val short_names: bool ref
-  val unique_names: bool ref
-end;
+type bstring = string;    (*primitive names to be bound*)
 
 signature BINDING =
 sig
-  include BASIC_BINDING
-  val name_pos: string * Position.T -> binding
-  val name: string -> binding
+  type binding
+  val dest: binding -> (string * bool) list * (string * bool) list * bstring
+  val str_of: binding -> string
+  val make: bstring * Position.T -> binding
+  val name: bstring -> binding
+  val pos_of: binding -> Position.T
+  val name_of: binding -> string
+  val map_name: (bstring -> bstring) -> binding -> binding
   val empty: binding
-  val map_base: (string -> string) -> binding -> binding
-  val qualify: string -> binding -> binding
+  val is_empty: binding -> bool
+  val qualify: bool -> string -> binding -> binding
+  val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   val add_prefix: bool -> string -> binding -> binding
-  val map_prefix: ((string * bool) list -> binding -> binding) -> binding -> binding
-  val is_empty: binding -> bool
-  val base_name: binding -> string
-  val pos_of: binding -> Position.T
-  val dest: binding -> (string * bool) list * string
-  val separator: string
-  val is_qualified: string -> bool
-  val display: binding -> string
 end;
 
-structure Binding : BINDING =
+structure Binding: BINDING =
 struct
 
-(** global flags **)
+(** representation **)
 
-val long_names = ref false;
-val short_names = ref false;
-val unique_names = ref true;
+(* datatype *)
 
+type component = string * bool;   (*name with mandatory flag*)
 
-(** qualification **)
-
-val separator = ".";
-val is_qualified = exists_string (fn s => s = separator);
+datatype binding = Binding of
+ {prefix: component list,         (*system prefix*)
+  qualifier: component list,      (*user qualifier*)
+  name: bstring,                  (*base name*)
+  pos: Position.T};               (*source position*)
 
-fun reject_qualified kind s =
-  if is_qualified s then
-    error ("Attempt to declare qualified " ^ kind ^ " " ^ quote s)
-  else s;
+fun make_binding (prefix, qualifier, name, pos) =
+  Binding {prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+
+fun map_binding f (Binding {prefix, qualifier, name, pos}) =
+  make_binding (f (prefix, qualifier, name, pos));
+
+fun dest (Binding {prefix, qualifier, name, ...}) = (prefix, qualifier, name);
 
 
-(** binding representation **)
+(* diagnostic output *)
 
-datatype binding = Binding of ((string * bool) list * string) * Position.T;
-  (* (prefix components (with mandatory flag), base name, position) *)
-
-fun name_pos (name, pos) = Binding (([], name), pos);
-fun name name = name_pos (name, Position.none);
-val empty = name "";
+val str_of_components = implode o map (fn (s, true) => s ^ "!" | (s, false) => s ^ "?");
 
-fun map_binding f (Binding (prefix_name, pos)) = Binding (f prefix_name, pos);
-
-val map_base = map_binding o apsnd;
+fun str_of (Binding {prefix, qualifier, name, pos}) =
+  let
+    val text =
+      (if null prefix then "" else enclose "(" ")" (str_of_components prefix)) ^
+      str_of_components qualifier ^ ":" ^ name;
+    val props = Position.properties_of pos;
+  in Markup.markup (Markup.properties props (Markup.binding name)) text end;
 
-fun qualify_base path name =
-  if path = "" orelse name = "" then name
-  else path ^ separator ^ name;
+
+
+(** basic operations **)
 
-val qualify = map_base o qualify_base;
-  (*FIXME should all operations on bare names move here from name_space.ML ?*)
+(* name and position *)
+
+fun make (name, pos) = make_binding ([], [], name, pos);
+fun name name = make (name, Position.none);
 
-fun add_prefix sticky "" b = b
-  | add_prefix sticky prfx b = (map_binding o apfst)
-      (cons ((*reject_qualified "prefix"*) prfx, sticky)) b;
+fun pos_of (Binding {pos, ...}) = pos;
+fun name_of (Binding {name, ...}) = name;
+
+fun map_name f = map_binding (fn (prefix, qualifier, name, pos) => (prefix, qualifier, f name, pos));
 
-fun map_prefix f (Binding ((prefix, name), pos)) =
-  f prefix (name_pos (name, pos));
+val empty = name "";
+fun is_empty b = name_of b = "";
+
+
+(* user qualifier *)
 
-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;
+fun qualify _ "" = I
+  | qualify mandatory qual = map_binding (fn (prefix, qualifier, name, pos) =>
+      (prefix, (qual, mandatory) :: qualifier, name, pos));
+
 
-fun display (Binding ((prefix, name), _)) =
-  let
-    fun mk_prefix (prfx, true) = prfx
-      | mk_prefix (prfx, false) = enclose "(" ")" prfx
-  in if not (! long_names) orelse null prefix orelse name = "" then name
-    else space_implode "." (map mk_prefix prefix) ^ ":" ^ name
-  end;
+(* system prefix *)
+
+fun map_prefix f = map_binding (fn (prefix, qualifier, name, pos) =>
+  (f prefix, qualifier, name, pos));
+
+fun add_prefix _ "" = I
+  | add_prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
 
 end;
 
-structure Basic_Binding : BASIC_BINDING = Binding;
-open Basic_Binding;
+type binding = Binding.binding;
+
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/markup.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -12,9 +12,9 @@
   val properties: (string * string) list -> T -> T
   val nameN: string
   val name: string -> T -> T
+  val bindingN: string val binding: string -> T
   val groupN: string
   val theory_nameN: string
-  val idN: string
   val kindN: string
   val internalK: string
   val property_internal: Properties.property
@@ -25,6 +25,7 @@
   val end_columnN: string
   val end_offsetN: string
   val fileN: string
+  val idN: string
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
@@ -107,6 +108,8 @@
 structure Markup: MARKUP =
 struct
 
+(** markup elements **)
+
 (* basic markup *)
 
 type T = string * Properties.T;
@@ -130,6 +133,8 @@
 val nameN = "name";
 fun name a = properties [(nameN, a)];
 
+val (bindingN, binding) = markup_string "binding" nameN;
+
 val groupN = "group";
 val theory_nameN = "theory_name";
 
@@ -278,7 +283,7 @@
 
 
 
-(* print mode operations *)
+(** print mode operations **)
 
 val no_output = ("", "");
 fun default_output (_: T) = no_output;
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -6,12 +6,18 @@
 Cf. Pure/General/binding.ML
 *)
 
-type bstring = string;    (*simple names to be bound -- legacy*)
 type xstring = string;    (*external names*)
 
+signature BASIC_NAME_SPACE =
+sig
+  val long_names: bool ref
+  val short_names: bool ref
+  val unique_names: bool ref
+end;
+
 signature NAME_SPACE =
 sig
-  include BASIC_BINDING
+  include BASIC_NAME_SPACE
   val hidden: string -> string
   val is_hidden: string -> bool
   val separator: string                 (*single char*)
@@ -27,8 +33,9 @@
   val empty: T
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
+  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
+    T -> string -> xstring
   val hide: bool -> string -> T -> T
-  val get_accesses: T -> string -> xstring list
   val merge: T * T -> T
   type naming
   val default_naming: naming
@@ -54,16 +61,13 @@
 structure NameSpace: NAME_SPACE =
 struct
 
-open Basic_Binding;
-
-
 (** long identifiers **)
 
 fun hidden name = "??." ^ name;
 val is_hidden = String.isPrefix "??.";
 
-val separator = Binding.separator;
-val is_qualified = Binding.is_qualified;
+val separator = ".";
+val is_qualified = exists_string (fn s => s = separator);
 
 val implode_name = space_implode separator;
 val explode_name = space_explode separator;
@@ -133,19 +137,10 @@
   | SOME ((name :: _, _), _) => (name, false)
   | SOME (([], name' :: _), _) => (hidden name', true));
 
-fun ex_mapsto_in (NameSpace (tab, _)) name xname =
-    (case Symtab.lookup tab xname of
-      SOME ((name'::_, _), _) => name' = name
-    | _ => false);
-
-fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
+fun get_accesses (NameSpace (_, tab)) name =
   (case Symtab.lookup tab name of
     NONE => [name]
-  | SOME (xnames, _) => if valid_only
-                        then filter (ex_mapsto_in ns name) xnames
-                        else xnames);
-
-val get_accesses = get_accesses' true;
+  | SOME (xnames, _) => xnames);
 
 fun put_accesses name xnames (NameSpace (tab, xtab)) =
   NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
@@ -158,20 +153,30 @@
 
 fun intern space xname = #1 (lookup space xname);
 
-fun extern space name =
+fun extern_flags {long_names, short_names, unique_names} space name =
   let
     fun valid unique xname =
       let val (name', uniq) = lookup space xname
       in name = name' andalso (uniq orelse not unique) end;
 
     fun ext [] = if valid false name then name else hidden name
-      | ext (nm :: nms) = if valid (! unique_names) nm then nm else ext nms;
+      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   in
-    if ! long_names then name
-    else if ! short_names then base name
-    else ext (get_accesses' false space name)
+    if long_names then name
+    else if short_names then base name
+    else ext (get_accesses space name)
   end;
 
+val long_names = ref false;
+val short_names = ref false;
+val unique_names = ref true;
+
+fun extern space name =
+  extern_flags
+   {long_names = ! long_names,
+    short_names = ! short_names,
+    unique_names = ! unique_names} space name;
+
 
 (* basic operations *)
 
@@ -203,7 +208,7 @@
       space
       |> add_name' name name
       |> fold (del_name name) (if fully then names else names inter_string [base name])
-      |> fold (del_name_extra name) (get_accesses' false space name)
+      |> fold (del_name_extra name) (get_accesses space name)
     end;
 
 
@@ -289,13 +294,13 @@
     in space |> fold (add_name name) accs |> put_accesses name accs' end;
 
 fun full_name naming b =
-  let val (prefix, bname) = Binding.dest b
-  in full_internal (apply_prefix prefix naming) bname end;
+  let val (prefix, qualifier, bname) = Binding.dest b
+  in full_internal (apply_prefix (prefix @ qualifier) naming) bname end;
 
 fun declare bnaming b =
   let
-    val (prefix, bname) = Binding.dest b;
-    val naming = apply_prefix prefix bnaming;
+    val (prefix, qualifier, bname) = Binding.dest b;
+    val naming = apply_prefix (prefix @ qualifier) bnaming;
     val name = full_internal naming bname;
   in declare_internal naming name #> pair name end;
 
@@ -331,3 +336,7 @@
 val explode = explode_name;
 
 end;
+
+structure BasicNameSpace: BASIC_NAME_SPACE = NameSpace;
+open BasicNameSpace;
+
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 03 18:33:21 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;
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -118,8 +118,7 @@
 fun attribute thy = attribute_i thy o intern_src thy;
 
 fun eval_thms ctxt args = ProofContext.note_thmss Thm.theoremK
-    [((Binding.empty, []),
-      map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
+    [(Thm.empty_binding, map (apsnd (map (attribute (ProofContext.theory_of ctxt)))) args)] ctxt
   |> fst |> maps snd;
 
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/class.ML	Tue Mar 03 18:33:21 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;
@@ -265,8 +265,7 @@
     |> add_consts bname class base_sort sups supparams global_syntax
     |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
           (map (fst o snd) params)
-          [((Binding.empty, []),
-            Option.map (globalize param_map) raw_pred |> the_list)]
+          [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
     #> snd
     #> `get_axiom
     #-> (fn assm_axiom => fold (Sign.add_const_constraint o apsnd SOME o snd) params
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/constdefs.ML
--- a/src/Pure/Isar/constdefs.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/constdefs.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -9,11 +9,9 @@
 signature CONSTDEFS =
 sig
   val add_constdefs: (binding * string option) list *
-    ((binding * string option * mixfix) option *
-      (Attrib.binding * string)) list -> theory -> theory
+    ((binding * string option * mixfix) option * (Attrib.binding * string)) list -> theory -> theory
   val add_constdefs_i: (binding * typ option) list *
-    ((binding * typ option * mixfix) option *
-      ((binding * attribute list) * term)) list -> theory -> theory
+    ((binding * typ option * mixfix) option * (Thm.binding * term)) list -> theory -> theory
 end;
 
 structure Constdefs: CONSTDEFS =
@@ -38,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
@@ -46,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' =
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/element.ML	Tue Mar 03 18:33:21 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)) =>
@@ -125,11 +125,9 @@
         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
 
 fun pretty_name_atts ctxt (b, atts) sep =
-  let val name = Binding.display b in
-    if name = "" andalso null atts then []
-    else [Pretty.block
-      (Pretty.breaks (Pretty.str name :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))]
-  end;
+  if Binding.is_empty b andalso null atts then []
+  else [Pretty.block (Pretty.breaks
+    (Pretty.str (Binding.str_of b) :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
 
 
 (* pretty_stmt *)
@@ -145,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))
@@ -170,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);
 
@@ -296,7 +294,7 @@
   gen_witness_proof (fn after_qed' => fn propss =>
     Proof.map_context (K goal_ctxt)
     #> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_i
-      cmd NONE after_qed' (map (pair (Binding.empty, [])) propss))
+      cmd NONE after_qed' (map (pair Thm.empty_binding) propss))
     (fn wits => fn _ => after_qed wits) wit_propss [];
 
 end;
@@ -504,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);
@@ -529,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,
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -88,17 +88,13 @@
         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
-      (if mx1 = mx2 then true
-      else error ("Conflicting syntax for parameter" ^ quote (Binding.display b1) ^
-                    " in expression."));
+      Binding.name_of b1 = Binding.name_of b2 andalso
+        (mx1 = mx2 orelse
+          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
       
-    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
-      (* FIXME: cannot compare bindings for equality. *)
-
     fun params_loc loc =
       (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =
@@ -133,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
@@ -310,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)
@@ -328,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;
 
@@ -360,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
@@ -394,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 *)
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 18:33:21 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);
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -11,8 +11,8 @@
   val mk_def: Proof.context -> (string * term) list -> term list
   val expand: cterm list -> thm -> thm
   val def_export: Assumption.export
-  val add_defs: ((binding * mixfix) * ((binding * attribute list) * term)) list ->
-    Proof.context -> (term * (string * thm)) list * Proof.context
+  val add_defs: ((binding * mixfix) * (Thm.binding * term)) list -> Proof.context ->
+    (term * (string * thm)) list * Proof.context
   val add_def: (binding * mixfix) * term -> Proof.context -> (term * thm) * Proof.context
   val fixed_abbrev: (binding * mixfix) * term -> Proof.context ->
     (term * term) * Proof.context
@@ -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
@@ -104,7 +104,7 @@
   end;
 
 fun add_def (var, rhs) ctxt =
-  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, ((Binding.empty, []), rhs))] ctxt
+  let val ([(lhs, (_, th))], ctxt') = add_defs [(var, (Thm.empty_binding, rhs))] ctxt
   in ((lhs, th), ctxt') end;
 
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Tue Mar 03 18:33:21 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], [])])];
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -40,11 +40,9 @@
 sig
   val thatN: string
   val obtain: string -> (binding * string option * mixfix) list ->
-    (Attrib.binding * (string * string list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
   val obtain_i: string -> (binding * typ option * mixfix) list ->
-    ((binding * attribute list) * (term * term list) list) list ->
-    bool -> Proof.state -> Proof.state
+    (Thm.binding * (term * term list) list) list -> bool -> Proof.state -> Proof.state
   val result: (Proof.context -> tactic) -> thm list -> Proof.context ->
     (cterm list * thm list) * Proof.context
   val guess: (binding * string option * mixfix) list -> bool -> Proof.state -> Proof.state
@@ -121,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);
@@ -155,14 +153,14 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K I) [((Binding.empty, []), [(obtain_prop, [])])] int
+    |> Proof.have_i NONE (K I) [(Thm.empty_binding, [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(Binding.name thesisN, NONE, NoSyn)]
     |> Proof.assume_i
       [((Binding.name that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [((Binding.empty, []), [(thesis, [])])] false
+    ||> Proof.show_i NONE after_qed [(Thm.empty_binding, [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -260,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;
 
@@ -295,7 +293,7 @@
         |> Proof.map_context (K ctxt')
         |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms)
         |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i
-          (obtain_export fix_ctxt rule (map cert ts)) [((Binding.empty, []), asms)])
+          (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)])
         |> Proof.add_binds_i AutoBind.no_facts
       end;
 
@@ -313,7 +311,7 @@
     |> Proof.fix_i [(Binding.name AutoBind.thesisN, NONE, NoSyn)]
     |> Proof.chain_facts chain_facts
     |> Proof.local_goal print_result (K I) (apsnd (rpair I))
-      "guess" before_qed after_qed [((Binding.empty, []), [Logic.mk_term goal, goal])]
+      "guess" before_qed after_qed [(Thm.empty_binding, [Logic.mk_term goal, goal])]
     |> Proof.refine (Method.primitive_text (K (Goal.init (cert thesis)))) |> Seq.hd
   end;
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Tue Mar 03 18:33:21 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;
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -48,23 +48,18 @@
   val assm: Assumption.export ->
     (Attrib.binding * (string * string list) list) list -> state -> state
   val assm_i: Assumption.export ->
-    ((binding * attribute list) * (term * term list) list) list -> state -> state
+    (Thm.binding * (term * term list) list) list -> state -> state
   val assume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val assume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
+  val assume_i: (Thm.binding * (term * term list) list) list -> state -> state
   val presume: (Attrib.binding * (string * string list) list) list -> state -> state
-  val presume_i: ((binding * attribute list) * (term * term list) list) list ->
-    state -> state
-  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list ->
-    state -> state
-  val def_i: ((binding * attribute list) *
-    ((binding * mixfix) * (term * term list))) list -> state -> state
+  val presume_i: (Thm.binding * (term * term list) list) list -> state -> state
+  val def: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
+  val def_i: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (Facts.ref * Attrib.src list) list -> thm list
   val note_thmss: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
-  val note_thmss_i: ((binding * attribute list) *
-    (thm list * attribute list) list) list -> state -> state
+  val note_thmss_i: (Thm.binding * (thm list * attribute list) list) list -> state -> state
   val from_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
   val from_thmss_i: ((thm list * attribute list) list) list -> state -> state
   val with_thmss: ((Facts.ref * Attrib.src list) list) list -> state -> state
@@ -107,11 +102,11 @@
   val have: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state) ->
     (Attrib.binding * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state) ->
-    ((binding * attribute list) * (term * term list) list) list -> bool -> state -> state
+    (Thm.binding * (term * term list) list) list -> bool -> state -> state
   val schematic_goal: state -> bool
   val is_relevant: state -> bool
   val local_future_proof: (state -> ('a * state) Future.future) ->
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -103,12 +103,10 @@
   val sticky_prefix: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
-  val note_thmss: string ->
-    ((binding * attribute list) * (Facts.ref * attribute list) list) list ->
-      Proof.context -> (string * thm list) list * Proof.context
-  val note_thmss_i: string ->
-    ((binding * attribute list) * (thm list * attribute list) list) list ->
-      Proof.context -> (string * thm list) list * Proof.context
+  val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
+  val note_thmss_i: string -> (Thm.binding * (thm list * attribute list) list) list ->
+    Proof.context -> (string * thm list) list * Proof.context
   val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
   val read_vars: (binding * string option * mixfix) list -> Proof.context ->
     (binding * typ option * mixfix) list * Proof.context
@@ -121,10 +119,10 @@
   val auto_fixes: Proof.context * (term list list * 'a) -> Proof.context * (term list list * 'a)
   val bind_fixes: string list -> Proof.context -> (term -> term) * Proof.context
   val add_assms: Assumption.export ->
-    ((binding * attribute list) * (string * string list) list) list ->
+    (Thm.binding * (string * string list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_assms_i: Assumption.export ->
-    ((binding * attribute list) * (term * term list) list) list ->
+    (Thm.binding * (term * term list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
   val add_cases: bool -> (string * RuleCases.T option) list -> Proof.context -> Proof.context
   val apply_case: RuleCases.T -> Proof.context -> (string * term list) list * Proof.context
@@ -1010,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);
@@ -1019,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
@@ -1093,7 +1091,7 @@
 fun add_abbrev mode tags (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
@@ -1120,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)
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Tue Mar 03 18:33:21 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
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Mar 03 18:33:21 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,
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -519,9 +519,9 @@
 fun ml_type txt = "val _ = NONE : (" ^ txt ^ ") option;";
 fun ml_struct txt = "functor DUMMY_FUNCTOR() = struct structure DUMMY = " ^ txt ^ " end;"
 
-fun output_ml ml src ctxt (txt, pos) =
+fun output_ml ml _ ctxt (txt, pos) =
  (ML_Context.eval_in (SOME ctxt) false pos (ml txt);
-  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
+  SymbolPos.content (SymbolPos.explode (txt, pos))
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   else
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -306,14 +306,11 @@
 
 fun nicer_shortest ctxt =
   let
-    val ns = ProofContext.theory_of ctxt
-             |> PureThy.facts_of
-             |> Facts.space_of;
+    (* FIXME global name space!? *)
+    val space = Facts.space_of (PureThy.facts_of (ProofContext.theory_of ctxt));
 
-    val len_sort = sort (int_ord o (pairself size));
-    fun shorten s = (case len_sort (NameSpace.get_accesses ns s) of
-                       [] => s
-                     | s'::_ => s');
+    val shorten =
+      NameSpace.extern_flags {long_names = false, short_names = false, unique_names = false} space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/axclass.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -8,7 +8,7 @@
 signature AX_CLASS =
 sig
   val define_class: bstring * class list -> string list ->
-    ((binding * attribute list) * term list) list -> theory -> class * theory
+    (Thm.binding * term list) list -> theory -> class * theory
   val add_classrel: thm -> theory -> theory
   val add_arity: thm -> theory -> theory
   val prove_classrel: class * class -> tactic -> theory -> theory
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/more_thm.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -40,6 +40,8 @@
   val close_derivation: thm -> thm
   val add_axiom: binding * term -> theory -> thm * theory
   val add_def: bool -> bool -> binding * term -> theory -> thm * theory
+  type binding = binding * attribute list
+  val empty_binding: binding
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
   val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
   val theory_attributes: attribute list -> theory * thm -> theory * thm
@@ -301,6 +303,9 @@
 
 (** attributes **)
 
+type binding = binding * attribute list;
+val empty_binding: binding = (Binding.empty, []);
+
 fun rule_attribute f (x, th) = (x, f x th);
 fun declaration_attribute f (x, th) = (f th x, th);
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/pure_setup.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -33,7 +33,7 @@
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
+install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.str_of));
 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/pure_thy.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -31,10 +31,10 @@
   val add_thm: (binding * thm) * attribute list -> theory -> thm * theory
   val add_thmss: ((binding * thm list) * attribute list) list -> theory -> thm list list * theory
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> theory -> theory
-  val note_thmss: string -> ((binding * attribute list) *
-    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
-  val note_thmss_grouped: string -> string -> ((binding * attribute list) *
-    (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss: string -> (Thm.binding *
+      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
+  val note_thmss_grouped: string -> string -> (Thm.binding *
+      (thm list * attribute list) list) list -> theory -> (string * thm list) list * theory
   val add_axioms: ((binding * term) * attribute list) list -> theory -> thm list * theory
   val add_axioms_cmd: ((bstring * string) * attribute list) list -> theory -> thm list * theory
   val add_defs: bool -> ((binding * term) * attribute list) list ->
@@ -151,14 +151,15 @@
 fun enter_thms pre_name post_name app_att (b, thms) thy =
   if Binding.is_empty b
   then swap (enter_proofs (app_att (thy, thms)))
-  else let
-    val naming = Sign.naming_of thy;
-    val name = NameSpace.full_name naming b;
-    val (thy', thms') =
-      enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
-    val thms'' = map (Thm.transfer thy') thms';
-    val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
-  in (thms'', thy'') end;
+  else
+    let
+      val naming = Sign.naming_of thy;
+      val name = NameSpace.full_name naming b;
+      val (thy', thms') =
+        enter_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
+      val thms'' = map (Thm.transfer thy') thms';
+      val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+    in (thms'', thy'') end;
 
 
 (* store_thm(s) *)
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/sign.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -507,12 +507,12 @@
     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.display b));
+          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT T;
       in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
@@ -549,7 +549,7 @@
     val pp = Syntax.pp_global thy;
     val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val (res, consts') = consts_of thy
       |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   in (res, thy |> map_consts (K consts')) end;
diff -r 79136ce06bdb -r 2bf6432b9740 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Pure/theory.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -258,7 +258,7 @@
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
-   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
+   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
 
 
diff -r 79136ce06bdb -r 2bf6432b9740 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/Tools/induct.ML	Tue Mar 03 18:33:21 2009 +0100
@@ -552,7 +552,7 @@
   let
     fun add (SOME (SOME x, t)) ctxt =
           let val ([(lhs, (_, th))], ctxt') =
-            LocalDefs.add_defs [((x, NoSyn), ((Binding.empty, []), t))] ctxt
+            LocalDefs.add_defs [((x, NoSyn), (Thm.empty_binding, t))] ctxt
           in ((SOME lhs, [th]), ctxt') end
       | add (SOME (NONE, t)) ctxt = ((SOME t, []), ctxt)
       | add NONE ctxt = ((NONE, []), ctxt);
diff -r 79136ce06bdb -r 2bf6432b9740 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Tue Mar 03 17:05:18 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Tue Mar 03 18:33:21 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;