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;
authorwenzelm
Tue Mar 03 18:32:01 2009 +0100 (2009-03-03)
changeset 3022324d975352879
parent 30222 4102bbf2af21
child 30225 2bf6432b9740
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;
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Tools/function_package/fundef_common.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_set_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Isar/args.ML
src/Pure/Isar/class.ML
src/Pure/Isar/constdefs.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/sign.ML
src/ZF/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 18:31:59 2009 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Mar 03 18:32:01 2009 +0100
     1.3 @@ -546,7 +546,7 @@
     1.4      Proof.theorem_i NONE (fn thss => fn ctxt =>
     1.5        let
     1.6          val rec_name = space_implode "_" (map Sign.base_name names);
     1.7 -        val rec_qualified = Binding.qualify rec_name;
     1.8 +        val rec_qualified = Binding.qualify false rec_name;
     1.9          val ind_case_names = RuleCases.case_names induct_cases;
    1.10          val induct_cases' = InductivePackage.partition_rules' raw_induct
    1.11            (intrs ~~ induct_cases); 
     2.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 18:31:59 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Tue Mar 03 18:32:01 2009 +0100
     2.3 @@ -453,7 +453,7 @@
     2.4      Proof.theorem_i NONE (fn thss => fn ctxt =>
     2.5        let
     2.6          val rec_name = space_implode "_" (map Sign.base_name names);
     2.7 -        val rec_qualified = Binding.qualify rec_name;
     2.8 +        val rec_qualified = Binding.qualify false rec_name;
     2.9          val ind_case_names = RuleCases.case_names induct_cases;
    2.10          val induct_cases' = InductivePackage.partition_rules' raw_induct
    2.11            (intrs ~~ induct_cases); 
     3.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 18:31:59 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Mar 03 18:32:01 2009 +0100
     3.3 @@ -210,7 +210,7 @@
     3.4      val def_name = Thm.def_name (Sign.base_name fname);
     3.5      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     3.6      val SOME var = get_first (fn ((b, _), mx) =>
     3.7 -      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
     3.8 +      if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
     3.9    in
    3.10      ((var, ((Binding.name def_name, []), rhs)),
    3.11       subst_bounds (rev (map Free frees), strip_abs_body rhs))
    3.12 @@ -248,7 +248,7 @@
    3.13      val (names_atts, spec') = split_list spec;
    3.14      val eqns' = map unquantify spec'
    3.15      val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
    3.16 -      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes)) spec' [];
    3.17 +      orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes)) spec' [];
    3.18      val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
    3.19      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
    3.20        map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
    3.21 @@ -285,7 +285,7 @@
    3.22        set_group ? LocalTheory.set_group (serial_string ()) |>
    3.23        fold_map (apfst (snd o snd) oo
    3.24          LocalTheory.define Thm.definitionK o fst) defs';
    3.25 -    val qualify = Binding.qualify
    3.26 +    val qualify = Binding.qualify false
    3.27        (space_implode "_" (map (Sign.base_name o #1) defs));
    3.28      val names_atts' = map (apfst qualify) names_atts;
    3.29      val cert = cterm_of (ProofContext.theory_of lthy');
     4.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 18:31:59 2009 +0100
     4.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Tue Mar 03 18:32:01 2009 +0100
     4.3 @@ -82,7 +82,7 @@
     4.4                                        psimps, pinducts, termination, defname}) phi =
     4.5      let
     4.6        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
     4.7 -      val name = Binding.base_name o Morphism.binding phi o Binding.name
     4.8 +      val name = Binding.name_of o Morphism.binding phi o Binding.name
     4.9      in
    4.10        FundefCtxData { add_simps = add_simps, case_names = case_names,
    4.11                        fs = map term fs, R = term R, psimps = fact psimps, 
     5.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 18:31:59 2009 +0100
     5.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Mar 03 18:32:01 2009 +0100
     5.3 @@ -99,8 +99,8 @@
     5.4        val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
     5.5        val ((fixes0, spec0), ctxt') = 
     5.6          prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
     5.7 -      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
     5.8 -      val spec = map (apfst (apfst Binding.base_name)) spec0;
     5.9 +      val fixes = map (apfst (apfst Binding.name_of)) fixes0;
    5.10 +      val spec = map (apfst (apfst Binding.name_of)) spec0;
    5.11        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    5.12  
    5.13        val defname = mk_defname fixes
     6.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Mar 03 18:31:59 2009 +0100
     6.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Mar 03 18:32:01 2009 +0100
     6.3 @@ -639,7 +639,7 @@
     6.4  
     6.5      val rec_name =
     6.6        if Binding.is_empty alt_name then
     6.7 -        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
     6.8 +        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
     6.9        else alt_name;
    6.10  
    6.11      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    6.12 @@ -674,9 +674,9 @@
    6.13  fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
    6.14        elims raw_induct ctxt =
    6.15    let
    6.16 -    val rec_name = Binding.base_name rec_binding;
    6.17 -    val rec_qualified = Binding.qualify rec_name;
    6.18 -    val intr_names = map Binding.base_name intr_bindings;
    6.19 +    val rec_name = Binding.name_of rec_binding;
    6.20 +    val rec_qualified = Binding.qualify false rec_name;
    6.21 +    val intr_names = map Binding.name_of intr_bindings;
    6.22      val ind_case_names = RuleCases.case_names intr_names;
    6.23      val induct =
    6.24        if coind then
    6.25 @@ -734,7 +734,7 @@
    6.26      cs intros monos params cnames_syn ctxt =
    6.27    let
    6.28      val _ = null cnames_syn andalso error "No inductive predicates given";
    6.29 -    val names = map (Binding.base_name o fst) cnames_syn;
    6.30 +    val names = map (Binding.name_of o fst) cnames_syn;
    6.31      val _ = message (quiet_mode andalso not verbose)
    6.32        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
    6.33  
    6.34 @@ -749,7 +749,7 @@
    6.35      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
    6.36        params intr_ts rec_preds_defs ctxt1;
    6.37      val elims = if no_elim then [] else
    6.38 -      prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
    6.39 +      prove_elims quiet_mode cs params intr_ts (map Binding.name_of intr_names)
    6.40          unfold rec_preds_defs ctxt1;
    6.41      val raw_induct = zero_var_indexes
    6.42        (if no_ind then Drule.asm_rl else
    6.43 @@ -793,7 +793,7 @@
    6.44  
    6.45      (* abbrevs *)
    6.46  
    6.47 -    val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
    6.48 +    val (_, ctxt1) = Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn) lthy;
    6.49  
    6.50      fun get_abbrev ((name, atts), t) =
    6.51        if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
    6.52 @@ -802,7 +802,7 @@
    6.53              error "Abbreviations may not have names or attributes";
    6.54            val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
    6.55            val var =
    6.56 -            (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
    6.57 +            (case find_first (fn ((c, _), _) => Binding.name_of c = x) cnames_syn of
    6.58                NONE => error ("Undeclared head of abbreviation " ^ quote x)
    6.59              | SOME ((b, T'), mx) =>
    6.60                  if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
    6.61 @@ -811,17 +811,17 @@
    6.62        else NONE;
    6.63  
    6.64      val abbrevs = map_filter get_abbrev spec;
    6.65 -    val bs = map (Binding.base_name o fst o fst) abbrevs;
    6.66 +    val bs = map (Binding.name_of o fst o fst) abbrevs;
    6.67  
    6.68  
    6.69      (* predicates *)
    6.70  
    6.71      val pre_intros = filter_out (is_some o get_abbrev) spec;
    6.72 -    val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
    6.73 -    val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
    6.74 +    val cnames_syn' = filter_out (member (op =) bs o Binding.name_of o fst o fst) cnames_syn;
    6.75 +    val cs = map (Free o apfst Binding.name_of o fst) cnames_syn';
    6.76      val ps = map Free pnames;
    6.77  
    6.78 -    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
    6.79 +    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.name_of o fst o fst) cnames_syn');
    6.80      val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
    6.81      val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
    6.82      val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
    6.83 @@ -854,7 +854,7 @@
    6.84    in
    6.85      lthy
    6.86      |> LocalTheory.set_group (serial_string ())
    6.87 -    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
    6.88 +    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
    6.89    end;
    6.90  
    6.91  val add_inductive_i = gen_add_inductive_i add_ind_def;
    6.92 @@ -954,7 +954,7 @@
    6.93                else if Binding.is_empty b then ((a, atts), B)
    6.94                else error "Illegal nested case names"
    6.95            | ((b, _), _) => error "Illegal simultaneous specification")
    6.96 -    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
    6.97 +    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.str_of a)));
    6.98  
    6.99  fun gen_ind_decl mk_def coind =
   6.100    P.fixes -- P.for_fixes --
     7.1 --- a/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 18:31:59 2009 +0100
     7.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Tue Mar 03 18:32:01 2009 +0100
     7.3 @@ -464,7 +464,7 @@
     7.4             | NONE => u)) |>
     7.5          Pattern.rewrite_term thy [] [to_pred_proc thy eqns'] |>
     7.6          eta_contract (member op = cs' orf is_pred pred_arities))) intros;
     7.7 -    val cnames_syn' = map (fn (b, _) => (Binding.map_base (suffix "p") b, NoSyn)) cnames_syn;
     7.8 +    val cnames_syn' = map (fn (b, _) => (Binding.map_name (suffix "p") b, NoSyn)) cnames_syn;
     7.9      val monos' = map (to_pred [] (Context.Proof ctxt)) monos;
    7.10      val ({preds, intrs, elims, raw_induct, ...}, ctxt1) =
    7.11        InductivePackage.add_ind_def
    7.12 @@ -501,7 +501,7 @@
    7.13      (* convert theorems to set notation *)
    7.14      val rec_name =
    7.15        if Binding.is_empty alt_name then
    7.16 -        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
    7.17 +        Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
    7.18        else alt_name;
    7.19      val cnames = map (LocalTheory.full_name ctxt3 o #1) cnames_syn;  (* FIXME *)
    7.20      val (intr_names, intr_atts) = split_list (map fst intros);
     8.1 --- a/src/HOL/Tools/primrec_package.ML	Tue Mar 03 18:31:59 2009 +0100
     8.2 +++ b/src/HOL/Tools/primrec_package.ML	Tue Mar 03 18:32:01 2009 +0100
     8.3 @@ -194,7 +194,7 @@
     8.4      val def_name = Thm.def_name (Sign.base_name fname);
     8.5      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     8.6      val SOME var = get_first (fn ((b, _), mx) =>
     8.7 -      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
     8.8 +      if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
     8.9    in (var, ((Binding.name def_name, []), rhs)) end;
    8.10  
    8.11  
    8.12 @@ -231,7 +231,7 @@
    8.13    let
    8.14      val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
    8.15      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
    8.16 -      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
    8.17 +      orelse exists (fn ((w, _), _) => v = Binding.name_of w) fixes) o snd) spec [];
    8.18      val tnames = distinct (op =) (map (#1 o snd) eqns);
    8.19      val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
    8.20      val main_fns = map (fn (tname, {index, ...}) =>
    8.21 @@ -248,7 +248,7 @@
    8.22        else primrec_error ("functions " ^ commas_quote names2 ^
    8.23          "\nare not mutually recursive");
    8.24      val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
    8.25 -    val qualify = Binding.qualify prefix;
    8.26 +    val qualify = Binding.qualify false prefix;
    8.27      val spec' = (map o apfst)
    8.28        (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
    8.29      val simp_atts = map (Attrib.internal o K)
    8.30 @@ -299,7 +299,7 @@
    8.31        P.name >> pair false) --| P.$$$ ")")) (false, "");
    8.32  
    8.33  val old_primrec_decl =
    8.34 -  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
    8.35 +  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop);
    8.36  
    8.37  fun pipe_error t = P.!!! (Scan.fail_with (K
    8.38    (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
     9.1 --- a/src/HOL/Tools/recdef_package.ML	Tue Mar 03 18:31:59 2009 +0100
     9.2 +++ b/src/HOL/Tools/recdef_package.ML	Tue Mar 03 18:32:01 2009 +0100
     9.3 @@ -320,7 +320,7 @@
     9.4  val _ =
     9.5    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
     9.6      K.thy_goal
     9.7 -    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
     9.8 +    ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.xname --
     9.9          Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    9.10        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    9.11  
    10.1 --- a/src/HOL/Tools/specification_package.ML	Tue Mar 03 18:31:59 2009 +0100
    10.2 +++ b/src/HOL/Tools/specification_package.ML	Tue Mar 03 18:32:01 2009 +0100
    10.3 @@ -232,7 +232,7 @@
    10.4  
    10.5  val specification_decl =
    10.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    10.7 -          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
    10.8 +          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop)
    10.9  
   10.10  val _ =
   10.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
   10.12 @@ -243,7 +243,7 @@
   10.13  val ax_specification_decl =
   10.14      P.name --
   10.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
   10.16 -           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
   10.17 +           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.name_of) -- P.prop))
   10.18  
   10.19  val _ =
   10.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
    11.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 18:31:59 2009 +0100
    11.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Tue Mar 03 18:32:01 2009 +0100
    11.3 @@ -175,7 +175,7 @@
    11.4    (spec : (Attrib.binding * term) list)
    11.5    (lthy : local_theory) =
    11.6    let
    11.7 -    val names = map (Binding.base_name o fst o fst) fixes;
    11.8 +    val names = map (Binding.name_of o fst o fst) fixes;
    11.9      val all_names = space_implode "_" names;
   11.10      val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
   11.11      val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
    12.1 --- a/src/Pure/Isar/args.ML	Tue Mar 03 18:31:59 2009 +0100
    12.2 +++ b/src/Pure/Isar/args.ML	Tue Mar 03 18:32:01 2009 +0100
    12.3 @@ -170,7 +170,7 @@
    12.4  val name_source_position = named >> T.source_position_of;
    12.5  
    12.6  val name = named >> T.content_of;
    12.7 -val binding = P.position name >> Binding.name_pos;
    12.8 +val binding = P.position name >> Binding.make;
    12.9  val alt_name = alt_string >> T.content_of;
   12.10  val symbol = symbolic >> T.content_of;
   12.11  val liberal_name = symbol || name;
    13.1 --- a/src/Pure/Isar/class.ML	Tue Mar 03 18:31:59 2009 +0100
    13.2 +++ b/src/Pure/Isar/class.ML	Tue Mar 03 18:32:01 2009 +0100
    13.3 @@ -201,7 +201,7 @@
    13.4        | check_element e = [()];
    13.5      val _ = map check_element syntax_elems;
    13.6      fun fork_syn (Element.Fixes xs) =
    13.7 -          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
    13.8 +          fold_map (fn (c, ty, syn) => cons (Binding.name_of c, syn) #> pair (c, ty, NoSyn)) xs
    13.9            #>> Element.Fixes
   13.10        | fork_syn x = pair x;
   13.11      val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
   13.12 @@ -228,7 +228,7 @@
   13.13      val raw_params = (snd o chop (length supparams)) all_params;
   13.14      fun add_const (b, SOME raw_ty, _) thy =
   13.15        let
   13.16 -        val v = Binding.base_name b;
   13.17 +        val v = Binding.name_of b;
   13.18          val c = Sign.full_bname thy v;
   13.19          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
   13.20          val ty0 = Type.strip_sorts ty;
    14.1 --- a/src/Pure/Isar/constdefs.ML	Tue Mar 03 18:31:59 2009 +0100
    14.2 +++ b/src/Pure/Isar/constdefs.ML	Tue Mar 03 18:32:01 2009 +0100
    14.3 @@ -36,7 +36,7 @@
    14.4      val prop = prep_prop var_ctxt raw_prop;
    14.5      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    14.6      val _ =
    14.7 -      (case Option.map Binding.base_name d of
    14.8 +      (case Option.map Binding.name_of d of
    14.9          NONE => ()
   14.10        | SOME c' =>
   14.11            if c <> c' then
   14.12 @@ -44,7 +44,7 @@
   14.13            else ());
   14.14  
   14.15      val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
   14.16 -    val name = Thm.def_name_optional c (Binding.base_name raw_name);
   14.17 +    val name = Thm.def_name_optional c (Binding.name_of raw_name);
   14.18      val atts = map (prep_att thy) raw_atts;
   14.19  
   14.20      val thy' =
    15.1 --- a/src/Pure/Isar/element.ML	Tue Mar 03 18:31:59 2009 +0100
    15.2 +++ b/src/Pure/Isar/element.ML	Tue Mar 03 18:32:01 2009 +0100
    15.3 @@ -96,7 +96,7 @@
    15.4  fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
    15.5    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    15.6     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    15.7 -      (Binding.base_name (binding (Binding.name x)), typ T)))
    15.8 +      (Binding.name_of (binding (Binding.name x)), typ T)))
    15.9     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
   15.10        ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
   15.11     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   15.12 @@ -143,8 +143,8 @@
   15.13        Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
   15.14  
   15.15      fun prt_var (x, SOME T) = Pretty.block
   15.16 -          [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
   15.17 -      | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
   15.18 +          [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
   15.19 +      | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
   15.20      val prt_vars = separate (Pretty.keyword "and") o map prt_var;
   15.21  
   15.22      fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
   15.23 @@ -168,9 +168,9 @@
   15.24      fun prt_mixfix NoSyn = []
   15.25        | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
   15.26  
   15.27 -    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
   15.28 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
   15.29            Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
   15.30 -      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
   15.31 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
   15.32            Pretty.brk 1 :: prt_mixfix mx);
   15.33      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
   15.34  
   15.35 @@ -502,7 +502,7 @@
   15.36          val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
   15.37          val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   15.38              let val ((c, _), t') = LocalDefs.cert_def ctxt t
   15.39 -            in (t', ((Binding.map_base (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
   15.40 +            in (t', ((Binding.map_name (Thm.def_name_optional c) name, atts), [(t', ps)])) end);
   15.41          val (_, ctxt') =
   15.42            ctxt |> fold (Variable.auto_fixes o #1) asms
   15.43            |> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
   15.44 @@ -527,7 +527,7 @@
   15.45  
   15.46  fun prep_facts prep_name get intern ctxt =
   15.47    map_ctxt
   15.48 -   {binding = Binding.map_base prep_name,
   15.49 +   {binding = Binding.map_name prep_name,
   15.50      typ = I,
   15.51      term = I,
   15.52      pattern = I,
    16.1 --- a/src/Pure/Isar/expression.ML	Tue Mar 03 18:31:59 2009 +0100
    16.2 +++ b/src/Pure/Isar/expression.ML	Tue Mar 03 18:32:01 2009 +0100
    16.3 @@ -88,10 +88,10 @@
    16.4          if null dups then () else error (message ^ commas dups)
    16.5        end;
    16.6  
    16.7 -    fun match_bind (n, b) = (n = Binding.base_name b);
    16.8 +    fun match_bind (n, b) = (n = Binding.name_of b);
    16.9      fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
   16.10        (* FIXME: cannot compare bindings for equality, instead check for equal name and syntax *)
   16.11 -      Binding.base_name b1 = Binding.base_name b2 andalso
   16.12 +      Binding.name_of b1 = Binding.name_of b2 andalso
   16.13          (mx1 = mx2 orelse
   16.14            error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
   16.15        
   16.16 @@ -129,8 +129,8 @@
   16.17  
   16.18      val (implicit, expr') = params_expr expr;
   16.19  
   16.20 -    val implicit' = map (#1 #> Binding.base_name) implicit;
   16.21 -    val fixed' = map (#1 #> Binding.base_name) fixed;
   16.22 +    val implicit' = map (#1 #> Binding.name_of) implicit;
   16.23 +    val fixed' = map (#1 #> Binding.name_of) fixed;
   16.24      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   16.25      val implicit'' = if strict then []
   16.26        else let val _ = reject_dups
   16.27 @@ -306,14 +306,12 @@
   16.28              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
   16.29          | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) =>
   16.30              let val ((c, _), t') = LocalDefs.cert_def ctxt (close_frees t)
   16.31 -            in
   16.32 -              ((Binding.map_base (Thm.def_name_optional c) name, atts), (t', no_binds ps))
   16.33 -            end))
   16.34 +            in ((Binding.map_name (Thm.def_name_optional c) name, atts), (t', no_binds ps)) end))
   16.35          | e => e)
   16.36        end;
   16.37  
   16.38  fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   16.39 -      let val x = Binding.base_name binding
   16.40 +      let val x = Binding.name_of binding
   16.41        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   16.42    | finish_primitive _ _ (Constrains _) = Constrains []
   16.43    | finish_primitive _ close (Assumes asms) = close (Assumes asms)
   16.44 @@ -324,7 +322,7 @@
   16.45    let
   16.46      val thy = ProofContext.theory_of ctxt;
   16.47      val (parm_names, parm_types) = Locale.params_of thy loc |>
   16.48 -      map_split (fn (b, SOME T, _) => (Binding.base_name b, T));
   16.49 +      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
   16.50      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   16.51    in (loc, morph) end;
   16.52  
   16.53 @@ -356,7 +354,7 @@
   16.54      fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
   16.55        let
   16.56          val (parm_names, parm_types) = Locale.params_of thy loc |>
   16.57 -          map_split (fn (b, SOME T, _) => (Binding.base_name b, T))
   16.58 +          map_split (fn (b, SOME T, _) => (Binding.name_of b, T))
   16.59              (*FIXME return value of Locale.params_of has strange type*)
   16.60          val inst' = prep_inst ctxt parm_names inst;
   16.61          val parm_types' = map (TypeInfer.paramify_vars o
   16.62 @@ -390,7 +388,7 @@
   16.63        prep_concl raw_concl (insts', elems, ctxt5);
   16.64  
   16.65      (* Retrieve parameter types *)
   16.66 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes)
   16.67 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.name_of o #1) fixes)
   16.68        | _ => fn ps => ps) (Fixes fors :: elems') [];
   16.69      val (Ts, ctxt7) = fold_map ProofContext.inferred_param xs ctxt6; 
   16.70      val parms = xs ~~ Ts;  (* params from expression and elements *)
    17.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 18:31:59 2009 +0100
    17.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Mar 03 18:32:01 2009 +0100
    17.3 @@ -161,7 +161,7 @@
    17.4  (* axioms *)
    17.5  
    17.6  fun add_axms f args thy =
    17.7 -  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    17.8 +  f (map (fn ((b, ax), srcs) => ((Binding.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    17.9  
   17.10  val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
   17.11  
    18.1 --- a/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:31:59 2009 +0100
    18.2 +++ b/src/Pure/Isar/local_defs.ML	Tue Mar 03 18:32:01 2009 +0100
    18.3 @@ -90,8 +90,8 @@
    18.4    let
    18.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
    18.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    18.7 -    val xs = map Binding.base_name bvars;
    18.8 -    val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
    18.9 +    val xs = map Binding.name_of bvars;
   18.10 +    val names = map2 (Binding.map_name o Thm.def_name_optional) xs bfacts;
   18.11      val eqs = mk_def ctxt (xs ~~ rhss);
   18.12      val lhss = map (fst o Logic.dest_equals) eqs;
   18.13    in
    19.1 --- a/src/Pure/Isar/locale.ML	Tue Mar 03 18:31:59 2009 +0100
    19.2 +++ b/src/Pure/Isar/locale.ML	Tue Mar 03 18:32:01 2009 +0100
    19.3 @@ -194,7 +194,7 @@
    19.4  fun axioms_of thy = #axioms o the_locale thy;
    19.5  
    19.6  fun instance_of thy name morph = params_of thy name |>
    19.7 -  map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
    19.8 +  map ((fn (b, T, _) => Free (Binding.name_of b, the T)) #> Morphism.term morph);
    19.9  
   19.10  fun specification_of thy = #spec o the_locale thy;
   19.11  
   19.12 @@ -464,8 +464,7 @@
   19.13  fun decl_attrib decl phi = Thm.declaration_attribute (K (decl phi));
   19.14  
   19.15  fun add_decls add loc decl =
   19.16 -  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ())))
   19.17 -    #>
   19.18 +  ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
   19.19    add_thmss loc Thm.internalK
   19.20      [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   19.21  
    20.1 --- a/src/Pure/Isar/obtain.ML	Tue Mar 03 18:31:59 2009 +0100
    20.2 +++ b/src/Pure/Isar/obtain.ML	Tue Mar 03 18:32:01 2009 +0100
    20.3 @@ -119,7 +119,7 @@
    20.4      (*obtain vars*)
    20.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    20.6      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    20.7 -    val xs = map (Binding.base_name o #1) vars;
    20.8 +    val xs = map (Binding.name_of o #1) vars;
    20.9  
   20.10      (*obtain asms*)
   20.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   20.12 @@ -258,7 +258,7 @@
   20.13  
   20.14  fun inferred_type (binding, _, mx) ctxt =
   20.15    let
   20.16 -    val x = Binding.base_name binding;
   20.17 +    val x = Binding.name_of binding;
   20.18      val (T, ctxt') = ProofContext.inferred_param x ctxt
   20.19    in ((x, T, mx), ctxt') end;
   20.20  
    21.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Mar 03 18:31:59 2009 +0100
    21.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Mar 03 18:32:01 2009 +0100
    21.3 @@ -228,7 +228,7 @@
    21.4  (* names and text *)
    21.5  
    21.6  val name = group "name declaration" (short_ident || sym_ident || string || number);
    21.7 -val binding = position name >> Binding.name_pos;
    21.8 +val binding = position name >> Binding.make;
    21.9  val xname = group "name reference" (short_ident || long_ident || sym_ident || string || number);
   21.10  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
   21.11  val path = group "file name/path specification" name >> Path.explode;
    22.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 18:31:59 2009 +0100
    22.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 18:32:01 2009 +0100
    22.3 @@ -1008,7 +1008,7 @@
    22.4  fun prep_vars prep_typ internal =
    22.5    fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
    22.6      let
    22.7 -      val raw_x = Binding.base_name raw_b;
    22.8 +      val raw_x = Binding.name_of raw_b;
    22.9        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
   22.10        val _ = Syntax.is_identifier (no_skolem internal x) orelse
   22.11          error ("Illegal variable name: " ^ quote x);
   22.12 @@ -1017,7 +1017,7 @@
   22.13          if internal then T
   22.14          else Type.no_tvars T handle TYPE (msg, _, _) => error msg;
   22.15        val opt_T = Option.map (cond_tvars o cert_typ ctxt o prep_typ ctxt) raw_T;
   22.16 -      val var = (Binding.map_base (K x) raw_b, opt_T, mx);
   22.17 +      val var = (Binding.map_name (K x) raw_b, opt_T, mx);
   22.18      in (var, ctxt |> declare_var (x, opt_T, mx) |> #2) end);
   22.19  
   22.20  in
   22.21 @@ -1118,7 +1118,7 @@
   22.22  fun gen_fixes prep raw_vars ctxt =
   22.23    let
   22.24      val (vars, _) = prep raw_vars ctxt;
   22.25 -    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
   22.26 +    val (xs', ctxt') = Variable.add_fixes (map (Binding.name_of o #1) vars) ctxt;
   22.27      val ctxt'' =
   22.28        ctxt'
   22.29        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    23.1 --- a/src/Pure/Isar/specification.ML	Tue Mar 03 18:31:59 2009 +0100
    23.2 +++ b/src/Pure/Isar/specification.ML	Tue Mar 03 18:32:01 2009 +0100
    23.3 @@ -140,7 +140,7 @@
    23.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
    23.5    let
    23.6      val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
    23.7 -    val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
    23.8 +    val xs = map (fn ((b, T), _) => (Binding.name_of b, T)) vars;
    23.9  
   23.10      (*consts*)
   23.11      val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
   23.12 @@ -148,8 +148,8 @@
   23.13  
   23.14      (*axioms*)
   23.15      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
   23.16 -        fold_map Thm.add_axiom
   23.17 -          ((map o apfst) Binding.name (PureThy.name_multi (Binding.base_name b) (map subst props)))
   23.18 +        fold_map Thm.add_axiom  (* FIXME proper use of binding!? *)
   23.19 +          ((map o apfst) Binding.name (PureThy.name_multi (Binding.name_of b) (map subst props)))
   23.20          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
   23.21      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
   23.22        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
   23.23 @@ -169,19 +169,19 @@
   23.24      val (vars, [((raw_name, atts), [prop])]) =
   23.25        fst (prep (the_list raw_var) [(raw_a, [raw_prop])] lthy);
   23.26      val (((x, T), rhs), prove) = LocalDefs.derived_def lthy true prop;
   23.27 -    val name = Binding.map_base (Thm.def_name_optional x) raw_name;
   23.28 +    val name = Binding.map_name (Thm.def_name_optional x) raw_name;
   23.29      val var =
   23.30        (case vars of
   23.31          [] => (Binding.name x, NoSyn)
   23.32        | [((b, _), mx)] =>
   23.33            let
   23.34 -            val y = Binding.base_name b;
   23.35 +            val y = Binding.name_of b;
   23.36              val _ = x = y orelse
   23.37                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
   23.38                  Position.str_of (Binding.pos_of b));
   23.39            in (b, mx) end);
   23.40      val ((lhs, (_, th)), lthy2) = lthy |> LocalTheory.define Thm.definitionK
   23.41 -        (var, ((Binding.map_base (suffix "_raw") name, []), rhs));
   23.42 +        (var, ((Binding.map_name (suffix "_raw") name, []), rhs));
   23.43      val ((def_name, [th']), lthy3) = lthy2 |> LocalTheory.note Thm.definitionK
   23.44          ((name, Code.add_default_eqn_attrib :: atts), [prove lthy2 th]);
   23.45  
   23.46 @@ -208,7 +208,7 @@
   23.47          [] => (Binding.name x, NoSyn)
   23.48        | [((b, _), mx)] =>
   23.49            let
   23.50 -            val y = Binding.base_name b;
   23.51 +            val y = Binding.name_of b;
   23.52              val _ = x = y orelse
   23.53                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   23.54                  Position.str_of (Binding.pos_of b));
   23.55 @@ -269,11 +269,10 @@
   23.56    | Element.Obtains obtains =>
   23.57        let
   23.58          val case_names = obtains |> map_index (fn (i, (b, _)) =>
   23.59 -          let val name = Binding.base_name b
   23.60 -          in if name = "" then string_of_int (i + 1) else name end);
   23.61 +          if Binding.is_empty b then string_of_int (i + 1) else Binding.name_of b);
   23.62          val constraints = obtains |> map (fn (_, (vars, _)) =>
   23.63            Element.Constrains
   23.64 -            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
   23.65 +            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.name_of x, T) | _ => NONE)));
   23.66  
   23.67          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
   23.68          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
   23.69 @@ -283,7 +282,7 @@
   23.70          fun assume_case ((name, (vars, _)), asms) ctxt' =
   23.71            let
   23.72              val bs = map fst vars;
   23.73 -            val xs = map Binding.base_name bs;
   23.74 +            val xs = map Binding.name_of bs;
   23.75              val props = map fst asms;
   23.76              val (Ts, _) = ctxt'
   23.77                |> fold Variable.declare_term props
    24.1 --- a/src/Pure/Isar/theory_target.ML	Tue Mar 03 18:31:59 2009 +0100
    24.2 +++ b/src/Pure/Isar/theory_target.ML	Tue Mar 03 18:32:01 2009 +0100
    24.3 @@ -188,8 +188,8 @@
    24.4      val arg = (b', Term.close_schematic_term rhs');
    24.5      val similar_body = Type.similar_types (rhs, rhs');
    24.6      (* FIXME workaround based on educated guess *)
    24.7 -    val (prefix', _) = Binding.dest b';
    24.8 -    val class_global = Binding.base_name b = Binding.base_name b'
    24.9 +    val (prefix', _, _) = Binding.dest b';
   24.10 +    val class_global = Binding.name_of b = Binding.name_of b'
   24.11        andalso not (null prefix')
   24.12        andalso (fst o snd o split_last) prefix' = Class_Target.class_prefix target;
   24.13    in
   24.14 @@ -206,14 +206,15 @@
   24.15               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   24.16    end;
   24.17  
   24.18 +fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   24.19 +
   24.20  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   24.21    let
   24.22 -    val c = Binding.base_name b;
   24.23 +    val c = Binding.name_of b;
   24.24      val tags = LocalTheory.group_position_of lthy;
   24.25      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   24.26      val U = map #2 xs ---> T;
   24.27      val (mx1, mx2, mx3) = fork_mixfix ta mx;
   24.28 -    fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
   24.29      val declare_const =
   24.30        (case Class_Target.instantiation_param lthy c of
   24.31          SOME c' =>
   24.32 @@ -241,7 +242,7 @@
   24.33  
   24.34  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   24.35    let
   24.36 -    val c = Binding.base_name b;
   24.37 +    val c = Binding.name_of b;
   24.38      val tags = LocalTheory.group_position_of lthy;
   24.39      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   24.40      val target_ctxt = LocalTheory.target_of lthy;
   24.41 @@ -278,8 +279,8 @@
   24.42      val thy = ProofContext.theory_of lthy;
   24.43      val thy_ctxt = ProofContext.init thy;
   24.44  
   24.45 -    val c = Binding.base_name b;
   24.46 -    val name' = Binding.map_base (Thm.def_name_optional c) name;
   24.47 +    val c = Binding.name_of b;
   24.48 +    val name' = Binding.map_name (Thm.def_name_optional c) name;
   24.49      val (rhs', rhs_conv) =
   24.50        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   24.51      val xs = Variable.add_fixed (LocalTheory.target_of lthy) rhs' [];
   24.52 @@ -299,7 +300,7 @@
   24.53            then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
   24.54            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   24.55      val (global_def, lthy3) = lthy2
   24.56 -      |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   24.57 +      |> LocalTheory.theory_result (define_const (Binding.name_of name') (lhs', rhs'));
   24.58      val def = LocalDefs.trans_terms lthy3
   24.59        [(*c == global.c xs*)     local_def,
   24.60         (*global.c xs == rhs'*)  global_def,
    25.1 --- a/src/Pure/sign.ML	Tue Mar 03 18:31:59 2009 +0100
    25.2 +++ b/src/Pure/sign.ML	Tue Mar 03 18:32:01 2009 +0100
    25.3 @@ -507,10 +507,10 @@
    25.4      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
    25.5      fun prep (raw_b, raw_T, raw_mx) =
    25.6        let
    25.7 -        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
    25.8 -        val b = Binding.map_base (K mx_name) raw_b;
    25.9 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.name_of raw_b) raw_mx;
   25.10 +        val b = Binding.map_name (K mx_name) raw_b;
   25.11          val c = full_name thy b;
   25.12 -        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
   25.13 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.name_of b;
   25.14          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   25.15            cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
   25.16          val T' = Logic.varifyT T;
    26.1 --- a/src/ZF/Tools/inductive_package.ML	Tue Mar 03 18:31:59 2009 +0100
    26.2 +++ b/src/ZF/Tools/inductive_package.ML	Tue Mar 03 18:32:01 2009 +0100
    26.3 @@ -65,7 +65,7 @@
    26.4    val _ = Theory.requires thy "Inductive_ZF" "(co)inductive definitions";
    26.5    val ctxt = ProofContext.init thy;
    26.6  
    26.7 -  val intr_specs = map (apfst (apfst Binding.base_name)) raw_intr_specs;
    26.8 +  val intr_specs = map (apfst (apfst Binding.name_of)) raw_intr_specs;
    26.9    val (intr_names, intr_tms) = split_list (map fst intr_specs);
   26.10    val case_names = RuleCases.case_names intr_names;
   26.11