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])]