Name.name_of -> Binding.base_name
authorhaftmann
Fri Dec 05 18:43:42 2008 +0100 (2008-12-05 ago)
changeset 29006abe0f11cfa4e
parent 29005 ce378dcfddab
child 29007 d808238131e7
Name.name_of -> Binding.base_name
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/General/binding.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/isar_syn.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/new_locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Tools/invoke.ML
src/Pure/name.ML
src/Pure/sign.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -230,7 +230,7 @@
     1.4  fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
     1.5    let
     1.6      val (raw_eqns, atts) = split_list eqns_atts;
     1.7 -    val eqns = map (apfst Name.name_of) raw_eqns;
     1.8 +    val eqns = map (apfst Binding.base_name) raw_eqns;
     1.9      val dt_info = NominalPackage.get_nominal_datatypes thy;
    1.10      val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
    1.11      val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
     2.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Dec 05 18:42:39 2008 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Dec 05 18:43:42 2008 +0100
     2.3 @@ -82,7 +82,7 @@
     2.4                                        psimps, pinducts, termination, defname}) phi =
     2.5      let
     2.6        val term = Morphism.term phi val thm = Morphism.thm phi val fact = Morphism.fact phi
     2.7 -      val name = Name.name_of o Morphism.binding phi o Binding.name
     2.8 +      val name = Binding.base_name o Morphism.binding phi o Binding.name
     2.9      in
    2.10        FundefCtxData { add_simps = add_simps, case_names = case_names,
    2.11                        fs = map term fs, R = term R, psimps = fact psimps, 
     3.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:42:39 2008 +0100
     3.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Fri Dec 05 18:43:42 2008 +0100
     3.3 @@ -96,8 +96,8 @@
     3.4  fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
     3.5      let
     3.6        val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
     3.7 -      val fixes = map (apfst (apfst Name.name_of)) fixes0;
     3.8 -      val spec = map (apfst (apfst Name.name_of)) spec0;
     3.9 +      val fixes = map (apfst (apfst Binding.base_name)) fixes0;
    3.10 +      val spec = map (apfst (apfst Binding.base_name)) spec0;
    3.11        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    3.12  
    3.13        val defname = mk_defname fixes
     4.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Dec 05 18:42:39 2008 +0100
     4.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Dec 05 18:43:42 2008 +0100
     4.3 @@ -260,7 +260,7 @@
     4.4  
     4.5  fun check_rule ctxt cs params ((binding, att), rule) =
     4.6    let
     4.7 -    val name = Name.name_of binding;
     4.8 +    val err_name = Binding.display binding;
     4.9      val params' = Term.variant_frees rule (Logic.strip_params rule);
    4.10      val frees = rev (map Free params');
    4.11      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
    4.12 @@ -278,7 +278,7 @@
    4.13  
    4.14      fun check_prem' prem t =
    4.15        if head_of t mem cs then
    4.16 -        check_ind (err_in_prem ctxt name rule prem) t
    4.17 +        check_ind (err_in_prem ctxt err_name rule prem) t
    4.18        else (case t of
    4.19            Abs (_, _, t) => check_prem' prem t
    4.20          | t $ u => (check_prem' prem t; check_prem' prem u)
    4.21 @@ -286,15 +286,15 @@
    4.22  
    4.23      fun check_prem (prem, aprem) =
    4.24        if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
    4.25 -      else err_in_prem ctxt name rule prem "Non-atomic premise";
    4.26 +      else err_in_prem ctxt err_name rule prem "Non-atomic premise";
    4.27    in
    4.28      (case concl of
    4.29         Const ("Trueprop", _) $ t =>
    4.30           if head_of t mem cs then
    4.31 -           (check_ind (err_in_rule ctxt name rule') t;
    4.32 +           (check_ind (err_in_rule ctxt err_name rule') t;
    4.33              List.app check_prem (prems ~~ aprems))
    4.34 -         else err_in_rule ctxt name rule' bad_concl
    4.35 -     | _ => err_in_rule ctxt name rule' bad_concl);
    4.36 +         else err_in_rule ctxt err_name rule' bad_concl
    4.37 +     | _ => err_in_rule ctxt err_name rule' bad_concl);
    4.38      ((binding, att), arule)
    4.39    end;
    4.40  
    4.41 @@ -638,7 +638,7 @@
    4.42  
    4.43      val rec_name =
    4.44        if Binding.is_empty alt_name then
    4.45 -        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
    4.46 +        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
    4.47        else alt_name;
    4.48  
    4.49      val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
    4.50 @@ -671,9 +671,9 @@
    4.51  fun declare_rules kind rec_binding coind no_ind cnames intrs intr_bindings intr_atts
    4.52        elims raw_induct ctxt =
    4.53    let
    4.54 -    val rec_name = Name.name_of rec_binding;
    4.55 +    val rec_name = Binding.base_name rec_binding;
    4.56      val rec_qualified = Binding.qualify rec_name;
    4.57 -    val intr_names = map Name.name_of intr_bindings;
    4.58 +    val intr_names = map Binding.base_name intr_bindings;
    4.59      val ind_case_names = RuleCases.case_names intr_names;
    4.60      val induct =
    4.61        if coind then
    4.62 @@ -730,11 +730,11 @@
    4.63      cs intros monos params cnames_syn ctxt =
    4.64    let
    4.65      val _ = null cnames_syn andalso error "No inductive predicates given";
    4.66 -    val names = map (Name.name_of o fst) cnames_syn;
    4.67 +    val names = map (Binding.base_name o fst) cnames_syn;
    4.68      val _ = message (quiet_mode andalso not verbose)
    4.69        ("Proofs for " ^ coind_prefix coind ^ "inductive predicate(s) " ^ commas_quote names);
    4.70  
    4.71 -    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt) o Name.name_of o #1) cnames_syn;  (* FIXME *)
    4.72 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt) o #1) cnames_syn;  (* FIXME *)
    4.73      val ((intr_names, intr_atts), intr_ts) =
    4.74        apfst split_list (split_list (map (check_rule ctxt cs params) intros));
    4.75  
    4.76 @@ -745,7 +745,7 @@
    4.77      val (intrs, unfold) = prove_intrs quiet_mode coind mono fp_def (length bs + length xs)
    4.78        params intr_ts rec_preds_defs ctxt1;
    4.79      val elims = if no_elim then [] else
    4.80 -      prove_elims quiet_mode cs params intr_ts (map Name.name_of intr_names)
    4.81 +      prove_elims quiet_mode cs params intr_ts (map Binding.base_name intr_names)
    4.82          unfold rec_preds_defs ctxt1;
    4.83      val raw_induct = zero_var_indexes
    4.84        (if no_ind then Drule.asm_rl else
    4.85 @@ -789,16 +789,16 @@
    4.86  
    4.87      (* abbrevs *)
    4.88  
    4.89 -    val (_, ctxt1) = Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn) lthy;
    4.90 +    val (_, ctxt1) = Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn) lthy;
    4.91  
    4.92      fun get_abbrev ((name, atts), t) =
    4.93        if can (Logic.strip_assums_concl #> Logic.dest_equals) t then
    4.94          let
    4.95 -          val _ = Name.name_of name = "" andalso null atts orelse
    4.96 +          val _ = Binding.is_empty name andalso null atts orelse
    4.97              error "Abbreviations may not have names or attributes";
    4.98            val ((x, T), rhs) = LocalDefs.abs_def (snd (LocalDefs.cert_def ctxt1 t));
    4.99            val var =
   4.100 -            (case find_first (fn ((c, _), _) => Name.name_of c = x) cnames_syn of
   4.101 +            (case find_first (fn ((c, _), _) => Binding.base_name c = x) cnames_syn of
   4.102                NONE => error ("Undeclared head of abbreviation " ^ quote x)
   4.103              | SOME ((b, T'), mx) =>
   4.104                  if T <> T' then error ("Bad type specification for abbreviation " ^ quote x)
   4.105 @@ -807,17 +807,17 @@
   4.106        else NONE;
   4.107  
   4.108      val abbrevs = map_filter get_abbrev spec;
   4.109 -    val bs = map (Name.name_of o fst o fst) abbrevs;
   4.110 +    val bs = map (Binding.base_name o fst o fst) abbrevs;
   4.111  
   4.112  
   4.113      (* predicates *)
   4.114  
   4.115      val pre_intros = filter_out (is_some o get_abbrev) spec;
   4.116 -    val cnames_syn' = filter_out (member (op =) bs o Name.name_of o fst o fst) cnames_syn;
   4.117 -    val cs = map (Free o apfst Name.name_of o fst) cnames_syn';
   4.118 +    val cnames_syn' = filter_out (member (op =) bs o Binding.base_name o fst o fst) cnames_syn;
   4.119 +    val cs = map (Free o apfst Binding.base_name o fst) cnames_syn';
   4.120      val ps = map Free pnames;
   4.121  
   4.122 -    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Name.name_of o fst o fst) cnames_syn');
   4.123 +    val (_, ctxt2) = lthy |> Variable.add_fixes (map (Binding.base_name o fst o fst) cnames_syn');
   4.124      val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
   4.125      val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
   4.126      val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
   4.127 @@ -849,7 +849,7 @@
   4.128    in
   4.129      lthy
   4.130      |> LocalTheory.set_group (serial_string ())
   4.131 -    |> gen_add_inductive_i mk_def flags cs (map (apfst Name.name_of o fst) ps) intrs monos
   4.132 +    |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.base_name o fst) ps) intrs monos
   4.133    end;
   4.134  
   4.135  val add_inductive_i = gen_add_inductive_i add_ind_def;
   4.136 @@ -857,7 +857,7 @@
   4.137  
   4.138  fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
   4.139    let
   4.140 -    val name = Sign.full_bname thy (Name.name_of (fst (fst (hd cnames_syn))));
   4.141 +    val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
   4.142      val ctxt' = thy
   4.143        |> TheoryTarget.init NONE
   4.144        |> LocalTheory.set_group group
   4.145 @@ -945,11 +945,11 @@
   4.146  fun flatten_specification specs = specs |> maps
   4.147    (fn (a, (concl, [])) => concl |> map
   4.148          (fn ((b, atts), [B]) =>
   4.149 -              if Name.name_of a = "" then ((b, atts), B)
   4.150 -              else if Name.name_of b = "" then ((a, atts), B)
   4.151 +              if Binding.is_empty a then ((b, atts), B)
   4.152 +              else if Binding.is_empty b then ((a, atts), B)
   4.153                else error "Illegal nested case names"
   4.154            | ((b, _), _) => error "Illegal simultaneous specification")
   4.155 -    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Name.name_of a)));
   4.156 +    | (a, _) => error ("Illegal local specification parameters for " ^ quote (Binding.base_name a)));
   4.157  
   4.158  fun gen_ind_decl mk_def coind =
   4.159    P.fixes -- P.for_fixes --
     5.1 --- a/src/HOL/Tools/inductive_set_package.ML	Fri Dec 05 18:42:39 2008 +0100
     5.2 +++ b/src/HOL/Tools/inductive_set_package.ML	Fri Dec 05 18:43:42 2008 +0100
     5.3 @@ -499,9 +499,9 @@
     5.4      (* convert theorems to set notation *)
     5.5      val rec_name =
     5.6        if Binding.is_empty alt_name then
     5.7 -        Binding.name (space_implode "_" (map (Name.name_of o fst) cnames_syn))
     5.8 +        Binding.name (space_implode "_" (map (Binding.base_name o fst) cnames_syn))
     5.9        else alt_name;
    5.10 -    val cnames = map (Sign.full_bname (ProofContext.theory_of ctxt3) o Name.name_of o #1) cnames_syn;  (* FIXME *)
    5.11 +    val cnames = map (Sign.full_name (ProofContext.theory_of ctxt3) o #1) cnames_syn;  (* FIXME *)
    5.12      val (intr_names, intr_atts) = split_list (map fst intros);
    5.13      val raw_induct' = to_set [] (Context.Proof ctxt3) raw_induct;
    5.14      val (intrs', elims', induct, ctxt4) =
     6.1 --- a/src/HOL/Tools/primrec_package.ML	Fri Dec 05 18:42:39 2008 +0100
     6.2 +++ b/src/HOL/Tools/primrec_package.ML	Fri Dec 05 18:43:42 2008 +0100
     6.3 @@ -194,7 +194,7 @@
     6.4      val def_name = Thm.def_name (Sign.base_name fname);
     6.5      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     6.6      val SOME var = get_first (fn ((b, _), mx) =>
     6.7 -      if Name.name_of b = fname then SOME (b, mx) else NONE) fixes;
     6.8 +      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
     6.9    in (var, ((Binding.name def_name, []), rhs)) end;
    6.10  
    6.11  
    6.12 @@ -231,7 +231,7 @@
    6.13    let
    6.14      val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
    6.15      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
    6.16 -      orelse exists (fn ((w, _), _) => v = Name.name_of w) fixes) o snd) spec [];
    6.17 +      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes) o snd) spec [];
    6.18      val tnames = distinct (op =) (map (#1 o snd) eqns);
    6.19      val dts = find_dts (DatatypePackage.get_datatypes (ProofContext.theory_of lthy)) tnames tnames;
    6.20      val main_fns = map (fn (tname, {index, ...}) =>
    6.21 @@ -298,7 +298,7 @@
    6.22        P.name >> pair false) --| P.$$$ ")")) (false, "");
    6.23  
    6.24  val old_primrec_decl =
    6.25 -  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop);
    6.26 +  opt_unchecked_name -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop);
    6.27  
    6.28  fun pipe_error t = P.!!! (Scan.fail_with (K
    6.29    (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
     7.1 --- a/src/HOL/Tools/recdef_package.ML	Fri Dec 05 18:42:39 2008 +0100
     7.2 +++ b/src/HOL/Tools/recdef_package.ML	Fri Dec 05 18:43:42 2008 +0100
     7.3 @@ -299,7 +299,7 @@
     7.4  
     7.5  val recdef_decl =
     7.6    Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true --
     7.7 -  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
     7.8 +  P.name -- P.term -- Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     7.9      -- Scan.option hints
    7.10    >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src);
    7.11  
    7.12 @@ -320,7 +320,7 @@
    7.13  val _ =
    7.14    OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
    7.15      K.thy_goal
    7.16 -    ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.xname --
    7.17 +    ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.xname --
    7.18          Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")")
    7.19        >> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
    7.20  
     8.1 --- a/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:42:39 2008 +0100
     8.2 +++ b/src/HOL/Tools/specification_package.ML	Fri Dec 05 18:43:42 2008 +0100
     8.3 @@ -233,7 +233,7 @@
     8.4  
     8.5  val specification_decl =
     8.6    P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
     8.7 -          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop)
     8.8 +          Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop)
     8.9  
    8.10  val _ =
    8.11    OuterSyntax.command "specification" "define constants by specification" K.thy_goal
    8.12 @@ -244,7 +244,7 @@
    8.13  val ax_specification_decl =
    8.14      P.name --
    8.15      (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" --
    8.16 -           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Name.name_of) -- P.prop))
    8.17 +           Scan.repeat1 ((SpecParse.opt_thm_name ":" >> apfst Binding.base_name) -- P.prop))
    8.18  
    8.19  val _ =
    8.20    OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal
     9.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Fri Dec 05 18:42:39 2008 +0100
     9.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Fri Dec 05 18:43:42 2008 +0100
     9.3 @@ -226,7 +226,7 @@
     9.4      val lengths = map length blocks;
     9.5      
     9.6      val ((bindings, srcss), strings) = apfst split_list (split_list eqns);
     9.7 -    val names = map Name.name_of bindings;
     9.8 +    val names = map Binding.base_name bindings;
     9.9      val atts = map (map (prep_attrib thy)) srcss;
    9.10      val eqn_ts = map (prep_prop thy) strings;
    9.11      val rec_ts = map (fn eq => chead_of (fst (dest_eqs (Logic.strip_imp_concl eq)))
    9.12 @@ -278,7 +278,7 @@
    9.13      val ts = map (prep_term thy) strings;
    9.14      val simps = map (fix_pat thy) ts;
    9.15    in
    9.16 -    (snd o PureThy.add_thmss [((Name.name_of name, simps), atts)]) thy
    9.17 +    (snd o PureThy.add_thmss [((Binding.base_name name, simps), atts)]) thy
    9.18    end;
    9.19  
    9.20  val add_fixpat = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
    10.1 --- a/src/Pure/General/binding.ML	Fri Dec 05 18:42:39 2008 +0100
    10.2 +++ b/src/Pure/General/binding.ML	Fri Dec 05 18:43:42 2008 +0100
    10.3 @@ -23,6 +23,7 @@
    10.4    val add_prefix: bool -> string -> T -> T
    10.5    val map_prefix: ((string * bool) list -> T -> T) -> T -> T
    10.6    val is_empty: T -> bool
    10.7 +  val base_name: T -> string
    10.8    val pos_of: T -> Position.T
    10.9    val dest: T -> (string * bool) list * string
   10.10    val display: T -> string
   10.11 @@ -56,7 +57,7 @@
   10.12    else path ^ "." ^ name;
   10.13  
   10.14  val qualify = map_base o qualify_base;
   10.15 -  (*FIXME should all operations on bare names moved here from name_space.ML ?*)
   10.16 +  (*FIXME should all operations on bare names move here from name_space.ML ?*)
   10.17  
   10.18  fun add_prefix sticky prfx b = if prfx = "" then error "empty name prefix"
   10.19    else (map_binding o apfst) (cons (prfx, sticky)) b;
   10.20 @@ -65,6 +66,7 @@
   10.21    f prefix (name_pos (name, pos));
   10.22  
   10.23  fun is_empty (Binding ((_, name), _)) = name = "";
   10.24 +fun base_name (Binding ((_, name), _)) = name;
   10.25  fun pos_of (Binding (_, pos)) = pos;
   10.26  fun dest (Binding (prefix_name, _)) = prefix_name;
   10.27  
    11.1 --- a/src/Pure/Isar/class.ML	Fri Dec 05 18:42:39 2008 +0100
    11.2 +++ b/src/Pure/Isar/class.ML	Fri Dec 05 18:43:42 2008 +0100
    11.3 @@ -545,7 +545,7 @@
    11.4      val constrain = Element.Constrains ((map o apsnd o map_atyps)
    11.5        (K (TFree (Name.aT, base_sort))) supparams);
    11.6      fun fork_syn (Element.Fixes xs) =
    11.7 -          fold_map (fn (c, ty, syn) => cons (Name.name_of c, syn) #> pair (c, ty, NoSyn)) xs
    11.8 +          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
    11.9            #>> Element.Fixes
   11.10        | fork_syn x = pair x;
   11.11      fun fork_syntax elems =
    12.1 --- a/src/Pure/Isar/constdefs.ML	Fri Dec 05 18:42:39 2008 +0100
    12.2 +++ b/src/Pure/Isar/constdefs.ML	Fri Dec 05 18:43:42 2008 +0100
    12.3 @@ -38,7 +38,7 @@
    12.4      val prop = prep_prop var_ctxt raw_prop;
    12.5      val (c, T) = #1 (LocalDefs.cert_def thy_ctxt (Logic.strip_imp_concl prop));
    12.6      val _ =
    12.7 -      (case Option.map Name.name_of d of
    12.8 +      (case Option.map Binding.base_name d of
    12.9          NONE => ()
   12.10        | SOME c' =>
   12.11            if c <> c' then
   12.12 @@ -46,7 +46,7 @@
   12.13            else ());
   12.14  
   12.15      val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_bname thy c, T))] prop;
   12.16 -    val name = Thm.def_name_optional c (Name.name_of raw_name);
   12.17 +    val name = Thm.def_name_optional c (Binding.base_name raw_name);
   12.18      val atts = map (prep_att thy) raw_atts;
   12.19  
   12.20      val thy' =
    13.1 --- a/src/Pure/Isar/element.ML	Fri Dec 05 18:42:39 2008 +0100
    13.2 +++ b/src/Pure/Isar/element.ML	Fri Dec 05 18:43:42 2008 +0100
    13.3 @@ -113,7 +113,7 @@
    13.4    fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
    13.5         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    13.6     | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    13.7 -       let val x' = Name.name_of (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    13.8 +       let val x' = Binding.base_name (#1 (var (Binding.name x, NoSyn))) in (x', typ T) end))
    13.9     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
   13.10        ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
   13.11     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
   13.12 @@ -136,7 +136,7 @@
   13.13  (* logical content *)
   13.14  
   13.15  fun params_of (Fixes fixes) = fixes |> map
   13.16 -    (fn (x, SOME T, _) => (Name.name_of x, T)
   13.17 +    (fn (x, SOME T, _) => (Binding.base_name x, T)
   13.18        | (x, _, _) => raise TERM ("Untyped context element parameter " ^ quote (Binding.display x), []))
   13.19    | params_of _ = [];
   13.20  
   13.21 @@ -182,8 +182,8 @@
   13.22        Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
   13.23  
   13.24      fun prt_var (x, SOME T) = Pretty.block
   13.25 -          [Pretty.str (Name.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
   13.26 -      | prt_var (x, NONE) = Pretty.str (Name.name_of x);
   13.27 +          [Pretty.str (Binding.base_name x ^ " ::"), Pretty.brk 1, prt_typ T]
   13.28 +      | prt_var (x, NONE) = Pretty.str (Binding.base_name x);
   13.29      val prt_vars = separate (Pretty.keyword "and") o map prt_var;
   13.30  
   13.31      fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
   13.32 @@ -207,9 +207,9 @@
   13.33      fun prt_mixfix NoSyn = []
   13.34        | prt_mixfix mx = [Pretty.brk 2, Syntax.pretty_mixfix mx];
   13.35  
   13.36 -    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Name.name_of x ^ " ::") ::
   13.37 +    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.base_name x ^ " ::") ::
   13.38            Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
   13.39 -      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Name.name_of x) ::
   13.40 +      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.base_name x) ::
   13.41            Pretty.brk 1 :: prt_mixfix mx);
   13.42      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
   13.43  
   13.44 @@ -395,7 +395,7 @@
   13.45  
   13.46  fun rename_var ren (b, mx) =
   13.47    let
   13.48 -    val x = Name.name_of b;
   13.49 +    val x = Binding.base_name b;
   13.50      val (x', mx') = rename_var_name ren (x, mx);
   13.51    in (Binding.name x', mx') end;
   13.52  
    14.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 05 18:42:39 2008 +0100
    14.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 05 18:43:42 2008 +0100
    14.3 @@ -134,8 +134,8 @@
    14.4          if null dups then () else error (message ^ commas dups)
    14.5        end;
    14.6  
    14.7 -    fun match_bind (n, b) = (n = Name.name_of b);
    14.8 -    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
    14.9 +    fun match_bind (n, b) = (n = Binding.base_name b);
   14.10 +    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
   14.11        (* FIXME: cannot compare bindings for equality. *)
   14.12  
   14.13      fun params_loc loc =
   14.14 @@ -177,8 +177,8 @@
   14.15  
   14.16      val (implicit, expr') = params_expr expr;
   14.17  
   14.18 -    val implicit' = map (#1 #> Name.name_of) implicit;
   14.19 -    val fixed' = map (#1 #> Name.name_of) fixed;
   14.20 +    val implicit' = map (#1 #> Binding.base_name) implicit;
   14.21 +    val fixed' = map (#1 #> Binding.base_name) fixed;
   14.22      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
   14.23      val implicit'' = if strict then []
   14.24        else let val _ = reject_dups
   14.25 @@ -385,7 +385,7 @@
   14.26        end;
   14.27  
   14.28  fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
   14.29 -      let val x = Name.name_of binding
   14.30 +      let val x = Binding.base_name binding
   14.31        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
   14.32    | finish_primitive _ _ (Constrains _) = Constrains []
   14.33    | finish_primitive _ close (Assumes asms) = close (Assumes asms)
   14.34 @@ -396,7 +396,7 @@
   14.35    let
   14.36      val thy = ProofContext.theory_of ctxt;
   14.37      val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   14.38 -      map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   14.39 +      map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
   14.40      val (asm, defs) = NewLocale.specification_of thy loc;
   14.41      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   14.42      val asm' = Option.map (Morphism.term morph) asm;
   14.43 @@ -440,7 +440,7 @@
   14.44      fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
   14.45        let
   14.46          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
   14.47 -          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
   14.48 +          map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
   14.49          val inst' = parse_inst parm_names inst ctxt;
   14.50          val parm_types' = map (TypeInfer.paramify_vars o
   14.51            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   14.52 @@ -473,7 +473,7 @@
   14.53      val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
   14.54  
   14.55      (* Retrieve parameter types *)
   14.56 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
   14.57 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
   14.58        _ => fn ps => ps) (Fixes fors :: elems) [];
   14.59      val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
   14.60      val parms = xs ~~ Ts;  (* params from expression and elements *)
    15.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 05 18:42:39 2008 +0100
    15.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Dec 05 18:43:42 2008 +0100
    15.3 @@ -167,7 +167,7 @@
    15.4  (* axioms *)
    15.5  
    15.6  fun add_axms f args thy =
    15.7 -  f (map (fn ((b, ax), srcs) => ((Name.name_of b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    15.8 +  f (map (fn ((b, ax), srcs) => ((Binding.base_name b, ax), map (Attrib.attribute thy) srcs)) args) thy;
    15.9  
   15.10  val add_axioms = add_axms (snd oo PureThy.add_axioms_cmd);
   15.11  
    16.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Dec 05 18:42:39 2008 +0100
    16.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Dec 05 18:43:42 2008 +0100
    16.3 @@ -413,7 +413,7 @@
    16.4        opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
    16.5          >> (fn ((name, expr), insts) => Toplevel.print o
    16.6              Toplevel.theory_to_proof
    16.7 -              (Locale.interpretation_cmd (Name.name_of name) expr insts)));
    16.8 +              (Locale.interpretation_cmd (Binding.base_name name) expr insts)));
    16.9  
   16.10  val _ =
   16.11    OuterSyntax.command "interpret"
   16.12 @@ -422,7 +422,7 @@
   16.13      (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
   16.14        >> (fn ((name, expr), insts) => Toplevel.print o
   16.15            Toplevel.proof'
   16.16 -            (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
   16.17 +            (fn int => Locale.interpret_cmd (Binding.base_name name) expr insts int)));
   16.18  
   16.19  
   16.20  (* classes *)
    17.1 --- a/src/Pure/Isar/local_defs.ML	Fri Dec 05 18:42:39 2008 +0100
    17.2 +++ b/src/Pure/Isar/local_defs.ML	Fri Dec 05 18:43:42 2008 +0100
    17.3 @@ -91,7 +91,7 @@
    17.4    let
    17.5      val ((bvars, mxs), specs) = defs |> split_list |>> split_list;
    17.6      val ((bfacts, atts), rhss) = specs |> split_list |>> split_list;
    17.7 -    val xs = map Name.name_of bvars;
    17.8 +    val xs = map Binding.base_name bvars;
    17.9      val names = map2 (Binding.map_base o Thm.def_name_optional) xs bfacts;
   17.10      val eqs = mk_def ctxt (xs ~~ rhss);
   17.11      val lhss = map (fst o Logic.dest_equals) eqs;
    18.1 --- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 18:42:39 2008 +0100
    18.2 +++ b/src/Pure/Isar/new_locale.ML	Fri Dec 05 18:43:42 2008 +0100
    18.3 @@ -175,7 +175,7 @@
    18.4  
    18.5  fun instance_of thy name morph =
    18.6    params_of thy name |>
    18.7 -    map ((fn (b, T, _) => Free (Name.name_of b, the T)) #> Morphism.term morph);
    18.8 +    map ((fn (b, T, _) => Free (Binding.base_name b, the T)) #> Morphism.term morph);
    18.9  
   18.10  fun specification_of thy name =
   18.11    let
    19.1 --- a/src/Pure/Isar/obtain.ML	Fri Dec 05 18:42:39 2008 +0100
    19.2 +++ b/src/Pure/Isar/obtain.ML	Fri Dec 05 18:43:42 2008 +0100
    19.3 @@ -122,7 +122,7 @@
    19.4      (*obtain vars*)
    19.5      val (vars, vars_ctxt) = prep_vars raw_vars ctxt;
    19.6      val (_, fix_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    19.7 -    val xs = map (Name.name_of o #1) vars;
    19.8 +    val xs = map (Binding.base_name o #1) vars;
    19.9  
   19.10      (*obtain asms*)
   19.11      val (asms_ctxt, proppss) = prep_propp (fix_ctxt, map snd raw_asms);
   19.12 @@ -261,7 +261,7 @@
   19.13  
   19.14  fun inferred_type (binding, _, mx) ctxt =
   19.15    let
   19.16 -    val x = Name.name_of binding;
   19.17 +    val x = Binding.base_name binding;
   19.18      val (T, ctxt') = ProofContext.inferred_param x ctxt
   19.19    in ((x, T, mx), ctxt') end;
   19.20  
    20.1 --- a/src/Pure/Isar/proof_context.ML	Fri Dec 05 18:42:39 2008 +0100
    20.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Dec 05 18:43:42 2008 +0100
    20.3 @@ -1012,7 +1012,7 @@
    20.4  fun prep_vars prep_typ internal =
    20.5    fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
    20.6      let
    20.7 -      val raw_x = Name.name_of raw_b;
    20.8 +      val raw_x = Binding.base_name raw_b;
    20.9        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
   20.10        val _ = Syntax.is_identifier (no_skolem internal x) orelse
   20.11          error ("Illegal variable name: " ^ quote x);
   20.12 @@ -1122,7 +1122,7 @@
   20.13  fun gen_fixes prep raw_vars ctxt =
   20.14    let
   20.15      val (vars, _) = prep raw_vars ctxt;
   20.16 -    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
   20.17 +    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
   20.18      val ctxt'' =
   20.19        ctxt'
   20.20        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)
    21.1 --- a/src/Pure/Isar/specification.ML	Fri Dec 05 18:42:39 2008 +0100
    21.2 +++ b/src/Pure/Isar/specification.ML	Fri Dec 05 18:43:42 2008 +0100
    21.3 @@ -153,7 +153,7 @@
    21.4  fun gen_axioms do_print prep raw_vars raw_specs thy =
    21.5    let
    21.6      val ((vars, specs), _) = prep raw_vars [raw_specs] (ProofContext.init thy);
    21.7 -    val xs = map (fn ((b, T), _) => (Name.name_of b, T)) vars;
    21.8 +    val xs = map (fn ((b, T), _) => (Binding.base_name b, T)) vars;
    21.9  
   21.10      (*consts*)
   21.11      val (consts, consts_thy) = thy |> fold_map (Theory.specify_const []) vars;
   21.12 @@ -161,7 +161,7 @@
   21.13  
   21.14      (*axioms*)
   21.15      val (axioms, axioms_thy) = consts_thy |> fold_map (fn ((b, atts), props) =>
   21.16 -        fold_map Thm.add_axiom (PureThy.name_multi (Name.name_of b) (map subst props))
   21.17 +        fold_map Thm.add_axiom (PureThy.name_multi (Binding.base_name b) (map subst props))
   21.18          #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])]))) specs;
   21.19      val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
   21.20        (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
   21.21 @@ -187,7 +187,7 @@
   21.22          [] => (Binding.name x, NoSyn)
   21.23        | [((b, _), mx)] =>
   21.24            let
   21.25 -            val y = Name.name_of b;
   21.26 +            val y = Binding.base_name b;
   21.27              val _ = x = y orelse
   21.28                error ("Head of definition " ^ quote x ^ " differs from declaration " ^ quote y ^
   21.29                  Position.str_of (Binding.pos_of b));
   21.30 @@ -220,7 +220,7 @@
   21.31          [] => (Binding.name x, NoSyn)
   21.32        | [((b, _), mx)] =>
   21.33            let
   21.34 -            val y = Name.name_of b;
   21.35 +            val y = Binding.base_name b;
   21.36              val _ = x = y orelse
   21.37                error ("Head of abbreviation " ^ quote x ^ " differs from declaration " ^ quote y ^
   21.38                  Position.str_of (Binding.pos_of b));
   21.39 @@ -281,11 +281,11 @@
   21.40    | Element.Obtains obtains =>
   21.41        let
   21.42          val case_names = obtains |> map_index (fn (i, (b, _)) =>
   21.43 -          let val name = Name.name_of b
   21.44 +          let val name = Binding.base_name b
   21.45            in if name = "" then string_of_int (i + 1) else name end);
   21.46          val constraints = obtains |> map (fn (_, (vars, _)) =>
   21.47            Element.Constrains
   21.48 -            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
   21.49 +            (vars |> map_filter (fn (x, SOME T) => SOME (Binding.base_name x, T) | _ => NONE)));
   21.50  
   21.51          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
   21.52          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
   21.53 @@ -295,7 +295,7 @@
   21.54          fun assume_case ((name, (vars, _)), asms) ctxt' =
   21.55            let
   21.56              val bs = map fst vars;
   21.57 -            val xs = map Name.name_of bs;
   21.58 +            val xs = map Binding.base_name bs;
   21.59              val props = map fst asms;
   21.60              val (Ts, _) = ctxt'
   21.61                |> fold Variable.declare_term props
    22.1 --- a/src/Pure/Isar/theory_target.ML	Fri Dec 05 18:42:39 2008 +0100
    22.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Dec 05 18:43:42 2008 +0100
    22.3 @@ -200,7 +200,7 @@
    22.4      val similar_body = Type.similar_types (rhs, rhs');
    22.5      (* FIXME workaround based on educated guess *)
    22.6      val (prefix', _) = Binding.dest b';
    22.7 -    val class_global = Name.name_of b = Name.name_of b'
    22.8 +    val class_global = Binding.base_name b = Binding.base_name b'
    22.9        andalso not (null prefix')
   22.10        andalso (fst o snd o split_last) prefix' = Class.class_prefix target;
   22.11    in
   22.12 @@ -219,7 +219,7 @@
   22.13  
   22.14  fun declare_const (ta as Target {target, is_locale, is_class, ...}) depends ((b, T), mx) lthy =
   22.15    let
   22.16 -    val c = Name.name_of b;
   22.17 +    val c = Binding.base_name b;
   22.18      val tags = LocalTheory.group_position_of lthy;
   22.19      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
   22.20      val U = map #2 xs ---> T;
   22.21 @@ -252,7 +252,7 @@
   22.22  
   22.23  fun abbrev (ta as Target {target, is_locale, is_class, ...}) prmode ((b, mx), t) lthy =
   22.24    let
   22.25 -    val c = Name.name_of b;
   22.26 +    val c = Binding.base_name b;
   22.27      val tags = LocalTheory.group_position_of lthy;
   22.28      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
   22.29      val target_ctxt = LocalTheory.target_of lthy;
   22.30 @@ -289,7 +289,7 @@
   22.31      val thy = ProofContext.theory_of lthy;
   22.32      val thy_ctxt = ProofContext.init thy;
   22.33  
   22.34 -    val c = Name.name_of b;
   22.35 +    val c = Binding.base_name b;
   22.36      val name' = Binding.map_base (Thm.def_name_optional c) name;
   22.37      val (rhs', rhs_conv) =
   22.38        LocalDefs.export_cterm lthy thy_ctxt (Thm.cterm_of thy rhs) |>> Thm.term_of;
   22.39 @@ -310,7 +310,7 @@
   22.40            then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   22.41            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   22.42      val (global_def, lthy3) = lthy2
   22.43 -      |> LocalTheory.theory_result (define_const (Name.name_of name') (lhs', rhs'));
   22.44 +      |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   22.45      val def = LocalDefs.trans_terms lthy3
   22.46        [(*c == global.c xs*)     local_def,
   22.47         (*global.c xs == rhs'*)  global_def,
    23.1 --- a/src/Pure/Tools/invoke.ML	Fri Dec 05 18:42:39 2008 +0100
    23.2 +++ b/src/Pure/Tools/invoke.ML	Fri Dec 05 18:43:42 2008 +0100
    23.3 @@ -120,7 +120,7 @@
    23.4      (K.tag_proof K.prf_goal)
    23.5      (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes
    23.6        >> (fn ((((name, atts), expr), (insts, _)), fixes) =>
    23.7 -          Toplevel.print o Toplevel.proof' (invoke (Name.name_of name, atts) expr insts fixes)));
    23.8 +          Toplevel.print o Toplevel.proof' (invoke (Binding.base_name name, atts) expr insts fixes)));
    23.9  
   23.10  end;
   23.11  
    24.1 --- a/src/Pure/name.ML	Fri Dec 05 18:42:39 2008 +0100
    24.2 +++ b/src/Pure/name.ML	Fri Dec 05 18:43:42 2008 +0100
    24.3 @@ -27,8 +27,6 @@
    24.4    val variants: string list -> context -> string list * context
    24.5    val variant_list: string list -> string list -> string list
    24.6    val variant: string list -> string -> string
    24.7 -
    24.8 -  val name_of: Binding.T -> string (*FIMXE legacy*)
    24.9  end;
   24.10  
   24.11  structure Name: NAME =
   24.12 @@ -140,9 +138,4 @@
   24.13  fun variant_list used names = #1 (make_context used |> variants names);
   24.14  fun variant used = singleton (variant_list used);
   24.15  
   24.16 -
   24.17 -(** generic name bindings -- legacy **)
   24.18 -
   24.19 -val name_of = snd o Binding.dest;
   24.20 -
   24.21  end;
    25.1 --- a/src/Pure/sign.ML	Fri Dec 05 18:42:39 2008 +0100
    25.2 +++ b/src/Pure/sign.ML	Fri Dec 05 18:43:42 2008 +0100
    25.3 @@ -508,10 +508,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 (Name.name_of raw_b) raw_mx;
    25.8 +        val (mx_name, mx) = Syntax.const_mixfix (Binding.base_name raw_b) raw_mx;
    25.9          val b = Binding.map_base (K mx_name) raw_b;
   25.10          val c = full_name thy b;
   25.11 -        val c_syn = if authentic then Syntax.constN ^ c else Name.name_of b;
   25.12 +        val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
   25.13          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
   25.14            cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
   25.15          val T' = Logic.varifyT T;
    26.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Dec 05 18:42:39 2008 +0100
    26.2 +++ b/src/ZF/Tools/inductive_package.ML	Fri Dec 05 18:43:42 2008 +0100
    26.3 @@ -67,7 +67,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 Name.name_of)) raw_intr_specs;
    26.8 +  val intr_specs = map (apfst (apfst Binding.base_name)) 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  
    27.1 --- a/src/ZF/Tools/primrec_package.ML	Fri Dec 05 18:42:39 2008 +0100
    27.2 +++ b/src/ZF/Tools/primrec_package.ML	Fri Dec 05 18:43:42 2008 +0100
    27.3 @@ -180,7 +180,7 @@
    27.4  
    27.5      val (eqn_thms', thy2) =
    27.6        thy1
    27.7 -      |> PureThy.add_thms ((map Name.name_of eqn_names ~~ eqn_thms) ~~ eqn_atts);
    27.8 +      |> PureThy.add_thms ((map Binding.base_name eqn_names ~~ eqn_thms) ~~ eqn_atts);
    27.9      val (_, thy3) =
   27.10        thy2
   27.11        |> PureThy.add_thmss [(("simps", eqn_thms'), [Simplifier.simp_add])]