1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 05 11:58:53 2009 +0100
1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Mar 05 12:08:00 2009 +0100
1.3 @@ -72,7 +72,7 @@
1.4 let
1.5 val thy = theory_of_thm thm;
1.6 (* the parsing function returns a qualified name, we get back the base name *)
1.7 - val atom_basename = Sign.base_name atom_name;
1.8 + val atom_basename = NameSpace.base_name atom_name;
1.9 val goal = List.nth(prems_of thm, i-1);
1.10 val ps = Logic.strip_params goal;
1.11 val Ts = rev (map snd ps);
1.12 @@ -159,7 +159,7 @@
1.13 NONE => all_tac thm
1.14 | SOME atom_name =>
1.15 let
1.16 - val atom_basename = Sign.base_name atom_name;
1.17 + val atom_basename = NameSpace.base_name atom_name;
1.18 val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
1.19 val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
1.20 fun inst_fresh vars params i st =
2.1 --- a/src/HOL/Nominal/nominal_inductive.ML Thu Mar 05 11:58:53 2009 +0100
2.2 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Mar 05 12:08:00 2009 +0100
2.3 @@ -199,7 +199,7 @@
2.4 val atomTs = distinct op = (maps (map snd o #2) prems);
2.5 val ind_sort = if null atomTs then HOLogic.typeS
2.6 else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
2.7 - ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs);
2.8 + ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs);
2.9 val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
2.10 val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
2.11 val fsT = TFree (fs_ctxt_tyname, ind_sort);
2.12 @@ -273,7 +273,7 @@
2.13
2.14 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
2.15 val pt2_atoms = map (fn aT => PureThy.get_thm thy
2.16 - ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
2.17 + ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
2.18 val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
2.19 addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
2.20 addsimprocs [mk_perm_bool_simproc ["Fun.id"],
2.21 @@ -281,7 +281,7 @@
2.22 val fresh_bij = PureThy.get_thms thy "fresh_bij";
2.23 val perm_bij = PureThy.get_thms thy "perm_bij";
2.24 val fs_atoms = map (fn aT => PureThy.get_thm thy
2.25 - ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
2.26 + ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
2.27 val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
2.28 val fresh_atm = PureThy.get_thms thy "fresh_atm";
2.29 val swap_simps = PureThy.get_thms thy "swap_simps";
2.30 @@ -545,7 +545,7 @@
2.31 ctxt'' |>
2.32 Proof.theorem_i NONE (fn thss => fn ctxt =>
2.33 let
2.34 - val rec_name = space_implode "_" (map Sign.base_name names);
2.35 + val rec_name = space_implode "_" (map NameSpace.base_name names);
2.36 val rec_qualified = Binding.qualify false rec_name;
2.37 val ind_case_names = RuleCases.case_names induct_cases;
2.38 val induct_cases' = InductivePackage.partition_rules' raw_induct
2.39 @@ -575,7 +575,7 @@
2.40 Attrib.internal (K (RuleCases.consumes 1))]),
2.41 strong_inducts) |> snd |>
2.42 LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
2.43 - ((Binding.name (NameSpace.qualified (Sign.base_name name) "strong_cases"),
2.44 + ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"),
2.45 [Attrib.internal (K (RuleCases.case_names (map snd cases))),
2.46 Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
2.47 (strong_cases ~~ induct_cases')) |> snd
2.48 @@ -665,7 +665,7 @@
2.49 in
2.50 ctxt |>
2.51 LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
2.52 - ((Binding.name (NameSpace.qualified (Sign.base_name name) "eqvt"),
2.53 + ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"),
2.54 [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
2.55 (names ~~ transp thss)) |> snd
2.56 end;
3.1 --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Mar 05 11:58:53 2009 +0100
3.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Mar 05 12:08:00 2009 +0100
3.3 @@ -229,7 +229,7 @@
3.4 val atoms = map (fst o dest_Type) atomTs;
3.5 val ind_sort = if null atomTs then HOLogic.typeS
3.6 else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
3.7 - ("fs_" ^ Sign.base_name a)) atoms);
3.8 + ("fs_" ^ NameSpace.base_name a)) atoms);
3.9 val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
3.10 val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
3.11 val fsT = TFree (fs_ctxt_tyname, ind_sort);
3.12 @@ -296,7 +296,7 @@
3.13
3.14 val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
3.15 val pt2_atoms = map (fn a => PureThy.get_thm thy
3.16 - ("pt_" ^ Sign.base_name a ^ "2")) atoms;
3.17 + ("pt_" ^ NameSpace.base_name a ^ "2")) atoms;
3.18 val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
3.19 addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
3.20 addsimprocs [mk_perm_bool_simproc ["Fun.id"],
3.21 @@ -324,7 +324,7 @@
3.22 val atom = fst (dest_Type T);
3.23 val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
3.24 val fs_atom = PureThy.get_thm thy
3.25 - ("fs_" ^ Sign.base_name atom ^ "1");
3.26 + ("fs_" ^ NameSpace.base_name atom ^ "1");
3.27 val avoid_th = Drule.instantiate'
3.28 [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
3.29 ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
3.30 @@ -452,7 +452,7 @@
3.31 ctxt'' |>
3.32 Proof.theorem_i NONE (fn thss => fn ctxt =>
3.33 let
3.34 - val rec_name = space_implode "_" (map Sign.base_name names);
3.35 + val rec_name = space_implode "_" (map NameSpace.base_name names);
3.36 val rec_qualified = Binding.qualify false rec_name;
3.37 val ind_case_names = RuleCases.case_names induct_cases;
3.38 val induct_cases' = InductivePackage.partition_rules' raw_induct
4.1 --- a/src/HOL/Nominal/nominal_package.ML Thu Mar 05 11:58:53 2009 +0100
4.2 +++ b/src/HOL/Nominal/nominal_package.ML Thu Mar 05 12:08:00 2009 +0100
4.3 @@ -49,9 +49,9 @@
4.4
4.5 fun dt_cases (descr: descr) (_, args, constrs) =
4.6 let
4.7 - fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
4.8 + fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i)));
4.9 val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
4.10 - in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
4.11 + in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
4.12
4.13
4.14 fun induct_cases descr =
4.15 @@ -364,7 +364,7 @@
4.16 val pi2 = Free ("pi2", permT);
4.17 val pt_inst = pt_inst_of thy2 a;
4.18 val pt2' = pt_inst RS pt2;
4.19 - val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
4.20 + val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a);
4.21 in List.take (map standard (split_conj_thm
4.22 (Goal.prove_global thy2 [] []
4.23 (augment_sort thy2 [pt_class_of thy2 a]
4.24 @@ -399,7 +399,7 @@
4.25 val pt_inst = pt_inst_of thy2 a;
4.26 val pt3' = pt_inst RS pt3;
4.27 val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
4.28 - val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
4.29 + val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a);
4.30 in List.take (map standard (split_conj_thm
4.31 (Goal.prove_global thy2 [] []
4.32 (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
4.33 @@ -664,7 +664,7 @@
4.34 asm_full_simp_tac (simpset_of thy addsimps
4.35 [Rep RS perm_closed RS Abs_inverse]) 1,
4.36 asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
4.37 - ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy
4.38 + ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy
4.39 end)
4.40 (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
4.41 new_type_names ~~ tyvars ~~ perm_closed_thms);
4.42 @@ -798,7 +798,7 @@
4.43 val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
4.44 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
4.45 (Const (rep_name, T --> T') $ lhs, rhs));
4.46 - val def_name = (Sign.base_name cname) ^ "_def";
4.47 + val def_name = (NameSpace.base_name cname) ^ "_def";
4.48 val ([def_thm], thy') = thy |>
4.49 Sign.add_consts_i [(cname', constrT, mx)] |>
4.50 (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
4.51 @@ -889,7 +889,7 @@
4.52 map (fn ((cname, dts), constr_rep_thm) =>
4.53 let
4.54 val cname = Sign.intern_const thy8
4.55 - (NameSpace.append tname (Sign.base_name cname));
4.56 + (NameSpace.append tname (NameSpace.base_name cname));
4.57 val permT = mk_permT (Type (atom, []));
4.58 val pi = Free ("pi", permT);
4.59
4.60 @@ -945,7 +945,7 @@
4.61 if null dts then NONE else SOME
4.62 let
4.63 val cname = Sign.intern_const thy8
4.64 - (NameSpace.append tname (Sign.base_name cname));
4.65 + (NameSpace.append tname (NameSpace.base_name cname));
4.66
4.67 fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
4.68 let
4.69 @@ -987,7 +987,7 @@
4.70 in List.concat (map (fn (cname, dts) => map (fn atom =>
4.71 let
4.72 val cname = Sign.intern_const thy8
4.73 - (NameSpace.append tname (Sign.base_name cname));
4.74 + (NameSpace.append tname (NameSpace.base_name cname));
4.75 val atomT = Type (atom, []);
4.76
4.77 fun process_constr ((dts, dt), (j, args1, args2)) =
4.78 @@ -1100,7 +1100,7 @@
4.79 (fn _ => indtac dt_induct indnames 1 THEN
4.80 ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
4.81 (abs_supp @ supp_atm @
4.82 - PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
4.83 + PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @
4.84 List.concat supp_thms))))),
4.85 length new_type_names))
4.86 end) atoms;
4.87 @@ -1232,9 +1232,9 @@
4.88 val fin_set_fresh = map (fn s =>
4.89 at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
4.90 val pt1_atoms = map (fn Type (s, _) =>
4.91 - PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
4.92 + PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs;
4.93 val pt2_atoms = map (fn Type (s, _) =>
4.94 - PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
4.95 + PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs;
4.96 val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
4.97 val fs_atoms = PureThy.get_thms thy9 "fin_supp";
4.98 val abs_supp = PureThy.get_thms thy9 "abs_supp";
4.99 @@ -1559,7 +1559,7 @@
4.100
4.101 val rec_fin_supp_thms = map (fn aT =>
4.102 let
4.103 - val name = Sign.base_name (fst (dest_Type aT));
4.104 + val name = NameSpace.base_name (fst (dest_Type aT));
4.105 val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
4.106 val aset = HOLogic.mk_setT aT;
4.107 val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
4.108 @@ -1598,7 +1598,7 @@
4.109
4.110 val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
4.111 let
4.112 - val name = Sign.base_name (fst (dest_Type aT));
4.113 + val name = NameSpace.base_name (fst (dest_Type aT));
4.114 val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
4.115 val a = Free ("a", aT);
4.116 val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
4.117 @@ -2012,10 +2012,10 @@
4.118 val (reccomb_defs, thy12) =
4.119 thy11
4.120 |> Sign.add_consts_i (map (fn ((name, T), T') =>
4.121 - (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
4.122 + (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
4.123 (reccomb_names ~~ recTs ~~ rec_result_Ts))
4.124 |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
4.125 - (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
4.126 + (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
4.127 Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
4.128 set $ Free ("x", T) $ Free ("y", T'))))))
4.129 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
5.1 --- a/src/HOL/Nominal/nominal_permeq.ML Thu Mar 05 11:58:53 2009 +0100
5.2 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Mar 05 12:08:00 2009 +0100
5.3 @@ -110,7 +110,7 @@
5.4 Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
5.5 (if (applicable_app f) then
5.6 let
5.7 - val name = Sign.base_name n
5.8 + val name = NameSpace.base_name n
5.9 val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
5.10 val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
5.11 in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
5.12 @@ -198,8 +198,8 @@
5.13 Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
5.14 pi2 $ t)) =>
5.15 let
5.16 - val tname' = Sign.base_name tname
5.17 - val uname' = Sign.base_name uname
5.18 + val tname' = NameSpace.base_name tname
5.19 + val uname' = NameSpace.base_name uname
5.20 in
5.21 if pi1 <> pi2 then (* only apply the composition rule in this case *)
5.22 if T = U then
6.1 --- a/src/HOL/Nominal/nominal_primrec.ML Thu Mar 05 11:58:53 2009 +0100
6.2 +++ b/src/HOL/Nominal/nominal_primrec.ML Thu Mar 05 12:08:00 2009 +0100
6.3 @@ -207,7 +207,7 @@
6.4 val frees = ls @ x :: rs;
6.5 val raw_rhs = list_abs_free (frees,
6.6 list_comb (Const (rec_name, dummyT), fs @ [Free x]))
6.7 - val def_name = Thm.def_name (Sign.base_name fname);
6.8 + val def_name = Thm.def_name (NameSpace.base_name fname);
6.9 val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
6.10 val SOME var = get_first (fn ((b, _), mx) =>
6.11 if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
6.12 @@ -286,7 +286,7 @@
6.13 fold_map (apfst (snd o snd) oo
6.14 LocalTheory.define Thm.definitionK o fst) defs';
6.15 val qualify = Binding.qualify false
6.16 - (space_implode "_" (map (Sign.base_name o #1) defs));
6.17 + (space_implode "_" (map (NameSpace.base_name o #1) defs));
6.18 val names_atts' = map (apfst qualify) names_atts;
6.19 val cert = cterm_of (ProofContext.theory_of lthy');
6.20
7.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 05 11:58:53 2009 +0100
7.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Mar 05 12:08:00 2009 +0100
7.3 @@ -115,7 +115,7 @@
7.4 (Var (n,ty))) =>
7.5 let
7.6 (* FIXME: this should be an operation the library *)
7.7 - val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
7.8 + val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
7.9 in
7.10 if (Sign.of_sort thy (ty,[class_name]))
7.11 then [(pi,typi)]
8.1 --- a/src/HOL/Statespace/state_fun.ML Thu Mar 05 11:58:53 2009 +0100
8.2 +++ b/src/HOL/Statespace/state_fun.ML Thu Mar 05 12:08:00 2009 +0100
8.3 @@ -336,17 +336,17 @@
8.4 [] => ""
8.5 | c::cs => String.implode (Char.toUpper c::cs ))
8.6
8.7 -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base T)
8.8 - | mkName (TFree (x,_)) = mkUpper (NameSpace.base x)
8.9 - | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base x);
8.10 +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T)
8.11 + | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x)
8.12 + | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x);
8.13
8.14 fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
8.15
8.16 -fun mk_map ("List.list") = Syntax.const "List.map"
8.17 - | mk_map n = Syntax.const ("StateFun." ^ "map_" ^ NameSpace.base n);
8.18 +fun mk_map "List.list" = Syntax.const "List.map"
8.19 + | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n);
8.20
8.21 fun gen_constr_destr comp prfx thy (Type (T,[])) =
8.22 - Syntax.const (deco prfx (mkUpper (NameSpace.base T)))
8.23 + Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))
8.24 | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
8.25 let val (argTs,rangeT) = strip_type T;
8.26 in comp
8.27 @@ -360,11 +360,11 @@
8.28 then (* datatype args are recursively embedded into val *)
8.29 (case argTs of
8.30 [argT] => comp
8.31 - ((Syntax.const (deco prfx (mkUpper (NameSpace.base T)))))
8.32 + ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))))
8.33 ((mk_map T $ gen_constr_destr comp prfx thy argT))
8.34 | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
8.35 else (* type args are not recursively embedded into val *)
8.36 - Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base T)))
8.37 + Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T)))
8.38 | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
8.39
8.40 val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
9.1 --- a/src/HOL/Statespace/state_space.ML Thu Mar 05 11:58:53 2009 +0100
9.2 +++ b/src/HOL/Statespace/state_space.ML Thu Mar 05 12:08:00 2009 +0100
9.3 @@ -645,7 +645,7 @@
9.4 fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
9.5
9.6 fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
9.7 - if NameSpace.base k = NameSpace.base KN then
9.8 + if NameSpace.base_name k = NameSpace.base_name KN then
9.9 (case get_comp (Context.Proof ctxt) name of
9.10 SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
9.11 Syntax.const "_statespace_update" $ s $ n $ v
10.1 --- a/src/HOL/Tools/TFL/post.ML Thu Mar 05 11:58:53 2009 +0100
10.2 +++ b/src/HOL/Tools/TFL/post.ML Thu Mar 05 12:08:00 2009 +0100
10.3 @@ -223,7 +223,7 @@
10.4 *---------------------------------------------------------------------------*)
10.5 fun define_i strict thy cs ss congs wfs fid R eqs =
10.6 let val {functional,pats} = Prim.mk_functional thy eqs
10.7 - val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
10.8 + val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional
10.9 val {induct, rules, tcs} =
10.10 simplify_defn strict thy cs ss congs wfs fid pats def
10.11 val rules' =
10.12 @@ -248,7 +248,7 @@
10.13
10.14 fun defer_i thy congs fid eqs =
10.15 let val {rules,R,theory,full_pats_TCs,SV,...} =
10.16 - Prim.lazyR_def thy (Sign.base_name fid) congs eqs
10.17 + Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs
10.18 val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
10.19 val dummy = writeln "Proving induction theorem ...";
10.20 val induction = Prim.mk_induction theory
11.1 --- a/src/HOL/Tools/TFL/tfl.ML Thu Mar 05 11:58:53 2009 +0100
11.2 +++ b/src/HOL/Tools/TFL/tfl.ML Thu Mar 05 12:08:00 2009 +0100
11.3 @@ -349,7 +349,7 @@
11.4 | L => mk_functional_err
11.5 ("The following clauses are redundant (covered by preceding clauses): " ^
11.6 commas (map (fn i => Int.toString (i + 1)) L))
11.7 - in {functional = Abs(Sign.base_name fname, ftype,
11.8 + in {functional = Abs(NameSpace.base_name fname, ftype,
11.9 abstract_over (atom,
11.10 absfree(aname,atype, case_tm))),
11.11 pats = patts2}
12.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Mar 05 11:58:53 2009 +0100
12.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Mar 05 12:08:00 2009 +0100
12.3 @@ -235,10 +235,10 @@
12.4 val (reccomb_defs, thy2) =
12.5 thy1
12.6 |> Sign.add_consts_i (map (fn ((name, T), T') =>
12.7 - (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
12.8 + (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
12.9 (reccomb_names ~~ recTs ~~ rec_result_Ts))
12.10 |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
12.11 - (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
12.12 + (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
12.13 Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
12.14 set $ Free ("x", T) $ Free ("y", T'))))))
12.15 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
12.16 @@ -316,8 +316,8 @@
12.17 val fns = (List.concat (Library.take (i, case_dummy_fns))) @
12.18 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
12.19 val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
12.20 - val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
12.21 - val def = (Binding.name (Sign.base_name name ^ "_def"),
12.22 + val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn);
12.23 + val def = (Binding.name (NameSpace.base_name name ^ "_def"),
12.24 Logic.mk_equals (list_comb (Const (name, caseT), fns1),
12.25 list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
12.26 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
13.1 --- a/src/HOL/Tools/datatype_aux.ML Thu Mar 05 11:58:53 2009 +0100
13.2 +++ b/src/HOL/Tools/datatype_aux.ML Thu Mar 05 12:08:00 2009 +0100
13.3 @@ -224,7 +224,7 @@
13.4 | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
13.5
13.6 fun name_of_typ (Type (s, Ts)) =
13.7 - let val s' = Sign.base_name s
13.8 + let val s' = NameSpace.base_name s
13.9 in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
13.10 [if Syntax.is_identifier s' then s' else "x"])
13.11 end
14.1 --- a/src/HOL/Tools/datatype_package.ML Thu Mar 05 11:58:53 2009 +0100
14.2 +++ b/src/HOL/Tools/datatype_package.ML Thu Mar 05 12:08:00 2009 +0100
14.3 @@ -174,9 +174,9 @@
14.4
14.5 fun dt_cases (descr: descr) (_, args, constrs) =
14.6 let
14.7 - fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i)));
14.8 + fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
14.9 val bnames = map the_bname (distinct (op =) (maps dt_recs args));
14.10 - in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
14.11 + in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
14.12
14.13
14.14 fun induct_cases descr =
14.15 @@ -519,7 +519,7 @@
14.16 val cs = map (apsnd (map norm_constr)) raw_cs;
14.17 val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
14.18 o fst o strip_type;
14.19 - val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
14.20 + val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
14.21
14.22 fun mk_spec (i, (tyco, constr)) = (i, (tyco,
14.23 map (DtTFree o fst) vs,
15.1 --- a/src/HOL/Tools/datatype_prop.ML Thu Mar 05 11:58:53 2009 +0100
15.2 +++ b/src/HOL/Tools/datatype_prop.ML Thu Mar 05 12:08:00 2009 +0100
15.3 @@ -47,7 +47,7 @@
15.4 let
15.5 fun type_name (TFree (name, _)) = implode (tl (explode name))
15.6 | type_name (Type (name, _)) =
15.7 - let val name' = Sign.base_name name
15.8 + let val name' = NameSpace.base_name name
15.9 in if Syntax.is_identifier name' then name' else "x" end;
15.10 in indexify_names (map type_name Ts) end;
15.11
16.1 --- a/src/HOL/Tools/datatype_realizer.ML Thu Mar 05 11:58:53 2009 +0100
16.2 +++ b/src/HOL/Tools/datatype_realizer.ML Thu Mar 05 12:08:00 2009 +0100
16.3 @@ -168,7 +168,7 @@
16.4 val Ts = map (typ_of_dtyp descr sorts) cargs;
16.5 val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
16.6 val free_ts = map Free frees;
16.7 - val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
16.8 + val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
16.9 in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
16.10 (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
16.11 HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
17.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 05 11:58:53 2009 +0100
17.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Mar 05 12:08:00 2009 +0100
17.3 @@ -236,7 +236,7 @@
17.4 val lhs = list_comb (Const (cname, constrT), l_args);
17.5 val rhs = mk_univ_inj r_args n i;
17.6 val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
17.7 - val def_name = Sign.base_name cname ^ "_def";
17.8 + val def_name = NameSpace.base_name cname ^ "_def";
17.9 val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
17.10 (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
17.11 val ([def_thm], thy') =
17.12 @@ -343,7 +343,7 @@
17.13
17.14 val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
17.15 val fTs = map fastype_of fs;
17.16 - val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
17.17 + val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"),
17.18 Logic.mk_equals (Const (iso_name, T --> Univ_elT),
17.19 list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
17.20 val (def_thms, thy') =
18.1 --- a/src/HOL/Tools/function_package/size.ML Thu Mar 05 11:58:53 2009 +0100
18.2 +++ b/src/HOL/Tools/function_package/size.ML Thu Mar 05 12:08:00 2009 +0100
18.3 @@ -87,7 +87,7 @@
18.4 recTs1 ~~ alt_names' |>
18.5 map (fn (T as Type (s, _), optname) =>
18.6 let
18.7 - val s' = the_default (Sign.base_name s) optname ^ "_size";
18.8 + val s' = the_default (NameSpace.base_name s) optname ^ "_size";
18.9 val s'' = Sign.full_bname thy s'
18.10 in
18.11 (s'',
18.12 @@ -140,7 +140,7 @@
18.13 val ((size_def_thms, size_def_thms'), thy') =
18.14 thy
18.15 |> Sign.add_consts_i (map (fn (s, T) =>
18.16 - (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
18.17 + (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
18.18 (size_names ~~ recTs1))
18.19 |> PureThy.add_defs false
18.20 (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
18.21 @@ -221,8 +221,8 @@
18.22 fun add_size_thms (new_type_names as name :: _) thy =
18.23 let
18.24 val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
18.25 - val prefix = NameSpace.map_base (K (space_implode "_"
18.26 - (the_default (map Sign.base_name new_type_names) alt_names))) name;
18.27 + val prefix = NameSpace.map_base_name (K (space_implode "_"
18.28 + (the_default (map NameSpace.base_name new_type_names) alt_names))) name;
18.29 val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
18.30 is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
18.31 in if no_size then thy
19.1 --- a/src/HOL/Tools/inductive_package.ML Thu Mar 05 11:58:53 2009 +0100
19.2 +++ b/src/HOL/Tools/inductive_package.ML Thu Mar 05 12:08:00 2009 +0100
19.3 @@ -698,7 +698,7 @@
19.4 ctxt1 |>
19.5 LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
19.6 fold_map (fn (name, (elim, cases)) =>
19.7 - LocalTheory.note kind ((Binding.name (NameSpace.qualified (Sign.base_name name) "cases"),
19.8 + LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
19.9 [Attrib.internal (K (RuleCases.case_names cases)),
19.10 Attrib.internal (K (RuleCases.consumes 1)),
19.11 Attrib.internal (K (Induct.cases_pred name)),
20.1 --- a/src/HOL/Tools/inductive_realizer.ML Thu Mar 05 11:58:53 2009 +0100
20.2 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Mar 05 12:08:00 2009 +0100
20.3 @@ -68,8 +68,8 @@
20.4 val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
20.5 (Logic.strip_imp_concl (prop_of (hd intrs))));
20.6 val params = map dest_Var (Library.take (nparms, ts));
20.7 - val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
20.8 - fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
20.9 + val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
20.10 + fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
20.11 map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
20.12 filter_out (equal Extraction.nullT) (map
20.13 (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
20.14 @@ -112,7 +112,7 @@
20.15 val rT = if n then Extraction.nullT
20.16 else Type (space_implode "_" (s ^ "T" :: vs),
20.17 map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
20.18 - val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
20.19 + val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT);
20.20 val S = list_comb (h, params @ xs);
20.21 val rvs = relevant_vars S;
20.22 val vs' = map fst rvs \\ vs;
20.23 @@ -195,7 +195,7 @@
20.24 in if conclT = Extraction.nullT
20.25 then list_abs_free (map dest_Free xs, HOLogic.unit)
20.26 else list_abs_free (map dest_Free xs, list_comb
20.27 - (Free ("r" ^ Sign.base_name (name_of_thm intr),
20.28 + (Free ("r" ^ NameSpace.base_name (name_of_thm intr),
20.29 map fastype_of (rev args) ---> conclT), rev args))
20.30 end
20.31
20.32 @@ -217,7 +217,7 @@
20.33 end) (premss ~~ dummies);
20.34 val frees = fold Term.add_frees fs [];
20.35 val Ts = map fastype_of fs;
20.36 - fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
20.37 + fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr)
20.38 in
20.39 fst (fold_map (fn concl => fn names =>
20.40 let val T = Extraction.etype_of thy vs [] concl
20.41 @@ -245,7 +245,7 @@
20.42 |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
20.43 handle DatatypeAux.Datatype_Empty name' =>
20.44 let
20.45 - val name = Sign.base_name name';
20.46 + val name = NameSpace.base_name name';
20.47 val dname = Name.variant used "Dummy"
20.48 in
20.49 thy
20.50 @@ -296,7 +296,7 @@
20.51
20.52 val thy1' = thy1 |>
20.53 Theory.copy |>
20.54 - Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
20.55 + Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
20.56 fold (fn s => AxClass.axiomatize_arity
20.57 (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
20.58 Extraction.add_typeof_eqns_i ty_eqs;
20.59 @@ -335,7 +335,7 @@
20.60 let
20.61 val Const (s, T) = head_of (HOLogic.dest_Trueprop
20.62 (Logic.strip_assums_concl rintr));
20.63 - val s' = Sign.base_name s;
20.64 + val s' = NameSpace.base_name s;
20.65 val T' = Logic.unvarifyT T
20.66 in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
20.67 val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
20.68 @@ -349,7 +349,7 @@
20.69 {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
20.70 coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
20.71 rlzpreds rlzparams (map (fn (rintr, intr) =>
20.72 - ((Binding.name (Sign.base_name (name_of_thm intr)), []),
20.73 + ((Binding.name (NameSpace.base_name (name_of_thm intr)), []),
20.74 subst_atomic rlzpreds' (Logic.unvarify rintr)))
20.75 (rintrs ~~ maps snd rss)) [] ||>
20.76 Sign.absolute_path;
21.1 --- a/src/HOL/Tools/old_primrec_package.ML Thu Mar 05 11:58:53 2009 +0100
21.2 +++ b/src/HOL/Tools/old_primrec_package.ML Thu Mar 05 12:08:00 2009 +0100
21.3 @@ -212,7 +212,7 @@
21.4 ((map snd ls) @ [dummyT])
21.5 (list_comb (Const (rec_name, dummyT),
21.6 fs @ map Bound (0 ::(length ls downto 1))))
21.7 - val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
21.8 + val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
21.9 val def_prop =
21.10 singleton (Syntax.check_terms (ProofContext.init thy))
21.11 (Logic.mk_equals (Const (fname, dummyT), rhs));
21.12 @@ -269,7 +269,7 @@
21.13 else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
21.14 "\nare not mutually recursive");
21.15 val primrec_name =
21.16 - if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
21.17 + if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
21.18 val (defs_thms', thy') =
21.19 thy
21.20 |> Sign.add_path primrec_name
22.1 --- a/src/HOL/Tools/primrec_package.ML Thu Mar 05 11:58:53 2009 +0100
22.2 +++ b/src/HOL/Tools/primrec_package.ML Thu Mar 05 12:08:00 2009 +0100
22.3 @@ -191,7 +191,7 @@
22.4 (map snd ls @ [dummyT])
22.5 (list_comb (Const (rec_name, dummyT),
22.6 fs @ map Bound (0 :: (length ls downto 1))))
22.7 - val def_name = Thm.def_name (Sign.base_name fname);
22.8 + val def_name = Thm.def_name (NameSpace.base_name fname);
22.9 val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
22.10 val SOME var = get_first (fn ((b, _), mx) =>
22.11 if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
22.12 @@ -247,7 +247,7 @@
22.13 val _ = if gen_eq_set (op =) (names1, names2) then ()
22.14 else primrec_error ("functions " ^ commas_quote names2 ^
22.15 "\nare not mutually recursive");
22.16 - val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
22.17 + val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs);
22.18 val qualify = Binding.qualify false prefix;
22.19 val spec' = (map o apfst)
22.20 (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
23.1 --- a/src/HOL/Tools/recdef_package.ML Thu Mar 05 11:58:53 2009 +0100
23.2 +++ b/src/HOL/Tools/recdef_package.ML Thu Mar 05 12:08:00 2009 +0100
23.3 @@ -193,7 +193,7 @@
23.4 val _ = requires_recdef thy;
23.5
23.6 val name = Sign.intern_const thy raw_name;
23.7 - val bname = Sign.base_name name;
23.8 + val bname = NameSpace.base_name name;
23.9 val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
23.10
23.11 val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
23.12 @@ -233,7 +233,7 @@
23.13 fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
23.14 let
23.15 val name = Sign.intern_const thy raw_name;
23.16 - val bname = Sign.base_name name;
23.17 + val bname = NameSpace.base_name name;
23.18
23.19 val _ = requires_recdef thy;
23.20 val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
24.1 --- a/src/HOL/Tools/record_package.ML Thu Mar 05 11:58:53 2009 +0100
24.2 +++ b/src/HOL/Tools/record_package.ML Thu Mar 05 12:08:00 2009 +0100
24.3 @@ -122,7 +122,7 @@
24.4 (* syntax *)
24.5
24.6 fun prune n xs = Library.drop (n, xs);
24.7 -fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);
24.8 +fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname);
24.9
24.10 val Trueprop = HOLogic.mk_Trueprop;
24.11 fun All xs t = Term.list_all_free (xs, t);
24.12 @@ -702,7 +702,7 @@
24.13 SOME flds
24.14 => (let
24.15 val (f::fs) = but_last (map fst flds);
24.16 - val flds' = Sign.extern_const thy f :: map NameSpace.base fs;
24.17 + val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs;
24.18 val (args',more) = split_last args;
24.19 in (flds'~~args')@field_lst more end
24.20 handle Library.UnequalLengths => [("",t)])
24.21 @@ -804,7 +804,7 @@
24.22 => (let
24.23 val (f :: fs) = but_last flds;
24.24 val flds' = apfst (Sign.extern_const thy) f
24.25 - :: map (apfst NameSpace.base) fs;
24.26 + :: map (apfst NameSpace.base_name) fs;
24.27 val (args', more) = split_last args;
24.28 val alphavars = map varifyT (but_last alphas);
24.29 val subst = fold2 (curry (Sign.typ_match thy))
24.30 @@ -1069,7 +1069,7 @@
24.31 val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
24.32
24.33 (*fun mk_abs_var x t = (x, fastype_of t);*)
24.34 - fun sel_name u = NameSpace.base (unsuffix updateN u);
24.35 + fun sel_name u = NameSpace.base_name (unsuffix updateN u);
24.36
24.37 fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
24.38 if has_field extfields s (domain_type' mT) then upd else seed s r
24.39 @@ -1463,7 +1463,7 @@
24.40 in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
24.41 in
24.42 thy
24.43 - |> TypecopyPackage.add_typecopy (suffix ext_typeN (Sign.base_name name), alphas) repT NONE
24.44 + |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
24.45 |-> (fn (name, _) => `(fn thy => get_thms thy name))
24.46 end;
24.47
24.48 @@ -1474,7 +1474,7 @@
24.49
24.50 fun extension_definition full name fields names alphas zeta moreT more vars thy =
24.51 let
24.52 - val base = Sign.base_name;
24.53 + val base = NameSpace.base_name;
24.54 val fieldTs = (map snd fields);
24.55 val alphas_zeta = alphas@[zeta];
24.56 val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
24.57 @@ -1760,7 +1760,7 @@
24.58 val alphas = map fst args;
24.59 val name = Sign.full_bname thy bname;
24.60 val full = Sign.full_bname_path thy bname;
24.61 - val base = Sign.base_name;
24.62 + val base = NameSpace.base_name;
24.63
24.64 val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
24.65
25.1 --- a/src/HOL/Tools/res_atp.ML Thu Mar 05 11:58:53 2009 +0100
25.2 +++ b/src/HOL/Tools/res_atp.ML Thu Mar 05 12:08:00 2009 +0100
25.3 @@ -380,7 +380,7 @@
25.4
25.5 (*Ignore blacklisted basenames*)
25.6 fun add_multi_names ((a, ths), pairs) =
25.7 - if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
25.8 + if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs
25.9 else add_single_names ((a, ths), pairs);
25.10
25.11 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
26.1 --- a/src/HOL/Tools/res_axioms.ML Thu Mar 05 11:58:53 2009 +0100
26.2 +++ b/src/HOL/Tools/res_axioms.ML Thu Mar 05 12:08:00 2009 +0100
26.3 @@ -342,7 +342,7 @@
26.4
26.5 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
26.6 fun skolem_thm (s, th) =
26.7 - if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then []
26.8 + if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
26.9 else
26.10 let
26.11 val ctxt0 = Variable.thm_context th
26.12 @@ -444,7 +444,7 @@
26.13 val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
26.14 if already_seen thy name then I else cons (name, ths));
26.15 val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
26.16 - if member (op =) multi_base_blacklist (Sign.base_name name) then I
26.17 + if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
26.18 else fold_index (fn (i, th) =>
26.19 if bad_for_atp th orelse is_some (lookup_cache thy th) then I
26.20 else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
27.1 --- a/src/HOL/Tools/specification_package.ML Thu Mar 05 11:58:53 2009 +0100
27.2 +++ b/src/HOL/Tools/specification_package.ML Thu Mar 05 12:08:00 2009 +0100
27.3 @@ -24,7 +24,7 @@
27.4 val ctype = domain_type (type_of P)
27.5 val cname_full = Sign.intern_const thy cname
27.6 val cdefname = if thname = ""
27.7 - then Thm.def_name (Sign.base_name cname)
27.8 + then Thm.def_name (NameSpace.base_name cname)
27.9 else thname
27.10 val def_eq = Logic.mk_equals (Const(cname_full,ctype),
27.11 HOLogic.choice_const ctype $ P)
27.12 @@ -50,7 +50,7 @@
27.13 val ctype = domain_type (type_of P)
27.14 val cname_full = Sign.intern_const thy cname
27.15 val cdefname = if thname = ""
27.16 - then Thm.def_name (Sign.base_name cname)
27.17 + then Thm.def_name (NameSpace.base_name cname)
27.18 else thname
27.19 val co = Const(cname_full,ctype)
27.20 val thy' = Theory.add_finals_i covld [co] thy
27.21 @@ -154,7 +154,7 @@
27.22 fun mk_exist (c,prop) =
27.23 let
27.24 val T = type_of c
27.25 - val cname = Sign.base_name (fst (dest_Const c))
27.26 + val cname = NameSpace.base_name (fst (dest_Const c))
27.27 val vname = if Syntax.is_identifier cname
27.28 then cname
27.29 else "x"
28.1 --- a/src/HOL/ex/Quickcheck_Generators.thy Thu Mar 05 11:58:53 2009 +0100
28.2 +++ b/src/HOL/ex/Quickcheck_Generators.thy Thu Mar 05 12:08:00 2009 +0100
28.3 @@ -138,7 +138,7 @@
28.4 let
28.5 val this_ty = Type (hd tycos, map TFree vs);
28.6 val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
28.7 - val random_name = NameSpace.base @{const_name random};
28.8 + val random_name = NameSpace.base_name @{const_name random};
28.9 val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
28.10 fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
28.11 val random' = Free (random'_name,
29.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML Thu Mar 05 11:58:53 2009 +0100
29.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Thu Mar 05 12:08:00 2009 +0100
29.3 @@ -22,7 +22,7 @@
29.4 val dc_rep = %%:(dname^"_rep");
29.5 val x_name'= "x";
29.6 val x_name = idx_name eqs x_name' (n+1);
29.7 - val dnam = Sign.base_name dname;
29.8 + val dnam = NameSpace.base_name dname;
29.9
29.10 val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
29.11 val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
30.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML Thu Mar 05 11:58:53 2009 +0100
30.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Thu Mar 05 12:08:00 2009 +0100
30.3 @@ -103,7 +103,7 @@
30.4 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
30.5 o fst) eqs''';
30.6 val cons''' = map snd eqs''';
30.7 - fun thy_type (dname,tvars) = (Sign.base_name dname, length tvars, NoSyn);
30.8 + fun thy_type (dname,tvars) = (NameSpace.base_name dname, length tvars, NoSyn);
30.9 fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS);
30.10 val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs)
30.11 |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
30.12 @@ -114,7 +114,7 @@
30.13 val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
30.14 fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
30.15 fun typid (Type (id,_)) =
30.16 - let val c = hd (Symbol.explode (Sign.base_name id))
30.17 + let val c = hd (Symbol.explode (NameSpace.base_name id))
30.18 in if Symbol.is_letter c then c else "t" end
30.19 | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id)))
30.20 | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
30.21 @@ -133,7 +133,7 @@
30.22 ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
30.23 in
30.24 theorems_thy
30.25 - |> Sign.add_path (Sign.base_name comp_dnam)
30.26 + |> Sign.add_path (NameSpace.base_name comp_dnam)
30.27 |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
30.28 |> Sign.parent_path
30.29 end;
31.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML Thu Mar 05 11:58:53 2009 +0100
31.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Thu Mar 05 12:08:00 2009 +0100
31.3 @@ -25,7 +25,7 @@
31.4 in
31.5 val dtype = Type(dname,typevars);
31.6 val dtype2 = foldr1 mk_ssumT (map prod cons');
31.7 - val dnam = Sign.base_name dname;
31.8 + val dnam = NameSpace.base_name dname;
31.9 val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
31.10 val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
31.11 val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
32.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML Thu Mar 05 11:58:53 2009 +0100
32.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Thu Mar 05 12:08:00 2009 +0100
32.3 @@ -606,7 +606,7 @@
32.4
32.5 in
32.6 thy
32.7 - |> Sign.add_path (Sign.base_name dname)
32.8 + |> Sign.add_path (NameSpace.base_name dname)
32.9 |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
32.10 ("iso_rews" , iso_rews ),
32.11 ("exhaust" , [exhaust] ),
33.1 --- a/src/HOLCF/Tools/fixrec_package.ML Thu Mar 05 11:58:53 2009 +0100
33.2 +++ b/src/HOLCF/Tools/fixrec_package.ML Thu Mar 05 12:08:00 2009 +0100
33.3 @@ -181,7 +181,7 @@
33.4 val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
33.5
33.6 fun one_def (l as Free(n,_)) r =
33.7 - let val b = Sign.base_name n
33.8 + let val b = NameSpace.base_name n
33.9 in ((Binding.name (b^"_def"), []), r) end
33.10 | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
33.11 fun defs [] _ = []
33.12 @@ -230,7 +230,7 @@
33.13
33.14 fun taken_names (t : term) : bstring list =
33.15 let
33.16 - fun taken (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
33.17 + fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
33.18 | taken (Free(a,_) , bs) = insert (op =) a bs
33.19 | taken (f $ u , bs) = taken (f, taken (u, bs))
33.20 | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
34.1 --- a/src/Pure/General/name_space.ML Thu Mar 05 11:58:53 2009 +0100
34.2 +++ b/src/Pure/General/name_space.ML Thu Mar 05 12:08:00 2009 +0100
34.3 @@ -25,9 +25,9 @@
34.4 val explode: string -> string list
34.5 val append: string -> string -> string
34.6 val qualified: string -> string -> string
34.7 - val base: string -> string
34.8 + val base_name: string -> string
34.9 val qualifier: string -> string
34.10 - val map_base: (string -> string) -> string -> string
34.11 + val map_base_name: (string -> string) -> string -> string
34.12 type T
34.13 val empty: T
34.14 val intern: T -> xstring -> string
34.15 @@ -78,14 +78,14 @@
34.16 if path = "" orelse name = "" then name
34.17 else path ^ separator ^ name;
34.18
34.19 -fun base "" = ""
34.20 - | base name = List.last (explode_name name);
34.21 +fun base_name "" = ""
34.22 + | base_name name = List.last (explode_name name);
34.23
34.24 fun qualifier "" = ""
34.25 | qualifier name = implode_name (#1 (split_last (explode_name name)));
34.26
34.27 -fun map_base _ "" = ""
34.28 - | map_base f name =
34.29 +fun map_base_name _ "" = ""
34.30 + | map_base_name f name =
34.31 let val names = explode_name name
34.32 in implode_name (nth_map (length names - 1) f names) end;
34.33
34.34 @@ -161,7 +161,7 @@
34.35 | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
34.36 in
34.37 if long_names then name
34.38 - else if short_names then base name
34.39 + else if short_names then base_name name
34.40 else ext (get_accesses space name)
34.41 end;
34.42
34.43 @@ -204,7 +204,7 @@
34.44 let val names = valid_accesses space name in
34.45 space
34.46 |> add_name' name name
34.47 - |> fold (del_name name) (if fully then names else names inter_string [base name])
34.48 + |> fold (del_name name) (if fully then names else names inter_string [base_name name])
34.49 |> fold (del_name_extra name) (get_accesses space name)
34.50 end;
34.51
35.1 --- a/src/Pure/Isar/class_target.ML Thu Mar 05 11:58:53 2009 +0100
35.2 +++ b/src/Pure/Isar/class_target.ML Thu Mar 05 12:08:00 2009 +0100
35.3 @@ -300,7 +300,7 @@
35.4 map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
35.5
35.6 fun redeclare_const thy c =
35.7 - let val b = Sign.base_name c
35.8 + let val b = NameSpace.base_name c
35.9 in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
35.10
35.11 fun synchronize_class_syntax sort base_sort ctxt =
35.12 @@ -358,7 +358,7 @@
35.13
35.14 (* class target *)
35.15
35.16 -val class_prefix = Logic.const_of_class o Sign.base_name;
35.17 +val class_prefix = Logic.const_of_class o NameSpace.base_name;
35.18
35.19 fun declare class pos ((c, mx), dict) thy =
35.20 let
35.21 @@ -475,7 +475,7 @@
35.22
35.23 fun type_name "*" = "prod"
35.24 | type_name "+" = "sum"
35.25 - | type_name s = sanatize_name (NameSpace.base s);
35.26 + | type_name s = sanatize_name (NameSpace.base_name s);
35.27
35.28 fun resort_terms pp algebra consts constraints ts =
35.29 let
36.1 --- a/src/Pure/Isar/element.ML Thu Mar 05 11:58:53 2009 +0100
36.2 +++ b/src/Pure/Isar/element.ML Thu Mar 05 12:08:00 2009 +0100
36.3 @@ -202,7 +202,7 @@
36.4 let val head =
36.5 if Thm.has_name_hint th then
36.6 Pretty.block [Pretty.command kind,
36.7 - Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
36.8 + Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")]
36.9 else Pretty.command kind
36.10 in Pretty.block (Pretty.fbreaks (head :: prts)) end;
36.11
37.1 --- a/src/Pure/Isar/proof_display.ML Thu Mar 05 11:58:53 2009 +0100
37.2 +++ b/src/Pure/Isar/proof_display.ML Thu Mar 05 12:08:00 2009 +0100
37.3 @@ -75,7 +75,7 @@
37.4
37.5 fun pretty_fact_name (kind, "") = Pretty.str kind
37.6 | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
37.7 - Pretty.str (NameSpace.base name), Pretty.str ":"];
37.8 + Pretty.str (NameSpace.base_name name), Pretty.str ":"];
37.9
37.10 fun pretty_facts ctxt =
37.11 flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
38.1 --- a/src/Pure/Isar/theory_target.ML Thu Mar 05 11:58:53 2009 +0100
38.2 +++ b/src/Pure/Isar/theory_target.ML Thu Mar 05 12:08:00 2009 +0100
38.3 @@ -330,7 +330,7 @@
38.4
38.5 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
38.6 Data.put ta #>
38.7 - LocalTheory.init (NameSpace.base target)
38.8 + LocalTheory.init (NameSpace.base_name target)
38.9 {pretty = pretty ta,
38.10 abbrev = abbrev ta,
38.11 define = define ta,
39.1 --- a/src/Pure/ML/ml_antiquote.ML Thu Mar 05 11:58:53 2009 +0100
39.2 +++ b/src/Pure/ML/ml_antiquote.ML Thu Mar 05 12:08:00 2009 +0100
39.3 @@ -110,7 +110,7 @@
39.4
39.5 fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
39.6 #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
39.7 - |> syn ? Sign.base_name
39.8 + |> syn ? NameSpace.base_name
39.9 |> ML_Syntax.print_string));
39.10
39.11 val _ = inline "type_name" (type_ false);
40.1 --- a/src/Pure/Thy/thm_deps.ML Thu Mar 05 11:58:53 2009 +0100
40.2 +++ b/src/Pure/Thy/thm_deps.ML Thu Mar 05 12:08:00 2009 +0100
40.3 @@ -33,7 +33,7 @@
40.4 | _ => ["global"]);
40.5 val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
40.6 val entry =
40.7 - {name = Sign.base_name name,
40.8 + {name = NameSpace.base_name name,
40.9 ID = name,
40.10 dir = space_implode "/" (session @ prefix),
40.11 unfold = false,
41.1 --- a/src/Pure/axclass.ML Thu Mar 05 11:58:53 2009 +0100
41.2 +++ b/src/Pure/axclass.ML Thu Mar 05 12:08:00 2009 +0100
41.3 @@ -158,7 +158,7 @@
41.4
41.5 (* maintain instances *)
41.6
41.7 -fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
41.8 +fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a;
41.9
41.10 val get_instances = #1 o #2 o AxClassData.get;
41.11 val map_instances = AxClassData.map o apsnd o apfst;
41.12 @@ -367,7 +367,7 @@
41.13 | NONE => error ("Illegal type for instantiation of class parameter: "
41.14 ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
41.15 val name_inst = instance_name (tyco, class) ^ "_inst";
41.16 - val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
41.17 + val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
41.18 val T' = Type.strip_sorts T;
41.19 in
41.20 thy
41.21 @@ -391,7 +391,7 @@
41.22 val (c', eq) = get_inst_param thy (c, tyco);
41.23 val prop = Logic.mk_equals (Const (c', T), t);
41.24 val name' = Thm.def_name_optional
41.25 - (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
41.26 + (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
41.27 in
41.28 thy
41.29 |> Thm.add_def false false (Binding.name name', prop)
42.1 --- a/src/Pure/consts.ML Thu Mar 05 11:58:53 2009 +0100
42.2 +++ b/src/Pure/consts.ML Thu Mar 05 12:08:00 2009 +0100
42.3 @@ -120,7 +120,7 @@
42.4 fun syntax consts (c, mx) =
42.5 let
42.6 val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
42.7 - val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
42.8 + val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c;
42.9 in (c', T, mx) end;
42.10
42.11 fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
43.1 --- a/src/Pure/logic.ML Thu Mar 05 11:58:53 2009 +0100
43.2 +++ b/src/Pure/logic.ML Thu Mar 05 12:08:00 2009 +0100
43.3 @@ -230,7 +230,7 @@
43.4 (* class relations *)
43.5
43.6 fun name_classrel (c1, c2) =
43.7 - NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
43.8 + NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
43.9
43.10 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
43.11
43.12 @@ -243,8 +243,8 @@
43.13 (* type arities *)
43.14
43.15 fun name_arities (t, _, S) =
43.16 - let val b = NameSpace.base t
43.17 - in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
43.18 + let val b = NameSpace.base_name t
43.19 + in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
43.20
43.21 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
43.22
44.1 --- a/src/Pure/old_term.ML Thu Mar 05 11:58:53 2009 +0100
44.2 +++ b/src/Pure/old_term.ML Thu Mar 05 12:08:00 2009 +0100
44.3 @@ -39,7 +39,7 @@
44.4
44.5 (*Accumulates the names in the term, suppressing duplicates.
44.6 Includes Frees and Consts. For choosing unambiguous bound var names.*)
44.7 -fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
44.8 +fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
44.9 | add_term_names (Free(a,_), bs) = insert (op =) a bs
44.10 | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
44.11 | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
45.1 --- a/src/Pure/primitive_defs.ML Thu Mar 05 11:58:53 2009 +0100
45.2 +++ b/src/Pure/primitive_defs.ML Thu Mar 05 12:08:00 2009 +0100
45.3 @@ -81,7 +81,7 @@
45.4 fun mk_defpair (lhs, rhs) =
45.5 (case Term.head_of lhs of
45.6 Const (name, _) =>
45.7 - (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
45.8 + (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
45.9 | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
45.10
45.11 end;
46.1 --- a/src/Pure/sign.ML Thu Mar 05 11:58:53 2009 +0100
46.2 +++ b/src/Pure/sign.ML Thu Mar 05 12:08:00 2009 +0100
46.3 @@ -14,7 +14,6 @@
46.4 consts: Consts.T}
46.5 val naming_of: theory -> NameSpace.naming
46.6 val full_name: theory -> binding -> string
46.7 - val base_name: string -> bstring
46.8 val full_bname: theory -> bstring -> string
46.9 val full_bname_path: theory -> string -> bstring -> string
46.10 val syn_of: theory -> Syntax.syntax
46.11 @@ -185,7 +184,6 @@
46.12 (* naming *)
46.13
46.14 val naming_of = #naming o rep_sg;
46.15 -val base_name = NameSpace.base;
46.16
46.17 val full_name = NameSpace.full_name o naming_of;
46.18 fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
47.1 --- a/src/Pure/term.ML Thu Mar 05 11:58:53 2009 +0100
47.2 +++ b/src/Pure/term.ML Thu Mar 05 12:08:00 2009 +0100
47.3 @@ -490,7 +490,7 @@
47.4
47.5 fun declare_term_names tm =
47.6 fold_aterms
47.7 - (fn Const (a, _) => Name.declare (NameSpace.base a)
47.8 + (fn Const (a, _) => Name.declare (NameSpace.base_name a)
47.9 | Free (a, _) => Name.declare a
47.10 | _ => I) tm #>
47.11 fold_types declare_typ_names tm;
47.12 @@ -721,7 +721,7 @@
47.13 fun lambda v t =
47.14 let val x =
47.15 (case v of
47.16 - Const (x, _) => NameSpace.base x
47.17 + Const (x, _) => NameSpace.base_name x
47.18 | Free (x, _) => x
47.19 | Var ((x, _), _) => x
47.20 | _ => Name.uu)
48.1 --- a/src/Tools/code/code_haskell.ML Thu Mar 05 11:58:53 2009 +0100
48.2 +++ b/src/Tools/code/code_haskell.ML Thu Mar 05 12:08:00 2009 +0100
48.3 @@ -34,7 +34,7 @@
48.4 fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
48.5 init_syms deresolve is_cons contr_classparam_typs deriving_show =
48.6 let
48.7 - val deresolve_base = NameSpace.base o deresolve;
48.8 + val deresolve_base = NameSpace.base_name o deresolve;
48.9 fun class_name class = case syntax_class class
48.10 of NONE => deresolve class
48.11 | SOME class => class;
48.12 @@ -143,7 +143,7 @@
48.13 @ str "="
48.14 :: str "error"
48.15 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
48.16 - o NameSpace.base o NameSpace.qualifier) name
48.17 + o NameSpace.base_name o NameSpace.qualifier) name
48.18 )
48.19 ]
48.20 end
48.21 @@ -155,7 +155,7 @@
48.22 let
48.23 val consts = map_filter
48.24 (fn c => if (is_some o syntax_const) c
48.25 - then NONE else (SOME o NameSpace.base o deresolve) c)
48.26 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
48.27 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
48.28 val vars = init_syms
48.29 |> Code_Name.intro_vars consts
48.30 @@ -255,7 +255,7 @@
48.31 let
48.32 val (c_inst_name, (_, tys)) = c_inst;
48.33 val const = if (is_some o syntax_const) c_inst_name
48.34 - then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
48.35 + then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name;
48.36 val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
48.37 val (vs, rhs) = unfold_abs_pure proto_rhs;
48.38 val vars = init_syms
48.39 @@ -360,7 +360,7 @@
48.40 val reserved_names = Code_Name.make_vars reserved_names;
48.41 fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
48.42 syntax_class syntax_tyco syntax_const reserved_names
48.43 - (if qualified then deresolver else NameSpace.base o deresolver)
48.44 + (if qualified then deresolver else NameSpace.base_name o deresolver)
48.45 is_cons contr_classparam_typs
48.46 (if string_classes then deriving_show else K false);
48.47 fun pr_module name content =
48.48 @@ -379,7 +379,7 @@
48.49 |> map_filter (try deresolver);
48.50 val qualified = is_none module_name andalso
48.51 map deresolver stmt_names @ deps'
48.52 - |> map NameSpace.base
48.53 + |> map NameSpace.base_name
48.54 |> has_duplicates (op =);
48.55 val imports = deps'
48.56 |> map NameSpace.qualifier
49.1 --- a/src/Tools/code/code_ml.ML Thu Mar 05 11:58:53 2009 +0100
49.2 +++ b/src/Tools/code/code_ml.ML Thu Mar 05 12:08:00 2009 +0100
49.3 @@ -47,7 +47,7 @@
49.4 let
49.5 val pr_label_classrel = translate_string (fn "." => "__" | c => c)
49.6 o NameSpace.qualifier;
49.7 - val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
49.8 + val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier;
49.9 fun pr_dicts fxy ds =
49.10 let
49.11 fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
49.12 @@ -163,7 +163,7 @@
49.13 fun pr_stmt (MLExc (name, n)) =
49.14 let
49.15 val exc_str =
49.16 - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
49.17 + (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
49.18 in
49.19 concat (
49.20 str (if n = 0 then "val" else "fun")
49.21 @@ -179,7 +179,7 @@
49.22 let
49.23 val consts = map_filter
49.24 (fn c => if (is_some o syntax_const) c
49.25 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.26 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.27 (Code_Thingol.fold_constnames (insert (op =)) t []);
49.28 val vars = reserved_names
49.29 |> Code_Name.intro_vars consts;
49.30 @@ -204,7 +204,7 @@
49.31 let
49.32 val consts = map_filter
49.33 (fn c => if (is_some o syntax_const) c
49.34 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.35 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.36 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
49.37 val vars = reserved_names
49.38 |> Code_Name.intro_vars consts
49.39 @@ -473,7 +473,7 @@
49.40 fun pr_stmt (MLExc (name, n)) =
49.41 let
49.42 val exc_str =
49.43 - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
49.44 + (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
49.45 in
49.46 concat (
49.47 str "let"
49.48 @@ -488,7 +488,7 @@
49.49 let
49.50 val consts = map_filter
49.51 (fn c => if (is_some o syntax_const) c
49.52 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.53 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.54 (Code_Thingol.fold_constnames (insert (op =)) t []);
49.55 val vars = reserved_names
49.56 |> Code_Name.intro_vars consts;
49.57 @@ -508,7 +508,7 @@
49.58 let
49.59 val consts = map_filter
49.60 (fn c => if (is_some o syntax_const) c
49.61 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.62 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.63 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
49.64 val vars = reserved_names
49.65 |> Code_Name.intro_vars consts
49.66 @@ -524,7 +524,7 @@
49.67 let
49.68 val consts = map_filter
49.69 (fn c => if (is_some o syntax_const) c
49.70 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.71 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.72 ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
49.73 val vars = reserved_names
49.74 |> Code_Name.intro_vars consts
49.75 @@ -552,7 +552,7 @@
49.76 let
49.77 val consts = map_filter
49.78 (fn c => if (is_some o syntax_const) c
49.79 - then NONE else (SOME o NameSpace.base o deresolve) c)
49.80 + then NONE else (SOME o NameSpace.base_name o deresolve) c)
49.81 ((fold o Code_Thingol.fold_constnames)
49.82 (insert (op =)) (map (snd o fst) eqs) []);
49.83 val vars = reserved_names
50.1 --- a/src/Tools/code/code_thingol.ML Thu Mar 05 11:58:53 2009 +0100
50.2 +++ b/src/Tools/code/code_thingol.ML Thu Mar 05 12:08:00 2009 +0100
50.3 @@ -246,15 +246,15 @@
50.4 in NameSpace.append prefix base end;
50.5 in
50.6
50.7 -fun namify_class thy = namify thy NameSpace.base thyname_of_class;
50.8 +fun namify_class thy = namify thy NameSpace.base_name thyname_of_class;
50.9 fun namify_classrel thy = namify thy (fn (class1, class2) =>
50.10 - NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
50.11 + NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst);
50.12 (*order fits nicely with composed projections*)
50.13 fun namify_tyco thy "fun" = "Pure.fun"
50.14 - | namify_tyco thy tyco = namify thy NameSpace.base thyname_of_tyco tyco;
50.15 + | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco;
50.16 fun namify_instance thy = namify thy (fn (class, tyco) =>
50.17 - NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
50.18 -fun namify_const thy = namify thy NameSpace.base thyname_of_const;
50.19 + NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance;
50.20 +fun namify_const thy = namify thy NameSpace.base_name thyname_of_const;
50.21
50.22 end; (* local *)
50.23
51.1 --- a/src/ZF/Tools/datatype_package.ML Thu Mar 05 11:58:53 2009 +0100
51.2 +++ b/src/ZF/Tools/datatype_package.ML Thu Mar 05 12:08:00 2009 +0100
51.3 @@ -74,7 +74,7 @@
51.4 Syntax.string_of_term_global thy t);
51.5
51.6 val rec_names = map (#1 o dest_Const) rec_hds
51.7 - val rec_base_names = map Sign.base_name rec_names
51.8 + val rec_base_names = map NameSpace.base_name rec_names
51.9 val big_rec_base_name = space_implode "_" rec_base_names
51.10
51.11 val thy_path = thy |> Sign.add_path big_rec_base_name
52.1 --- a/src/ZF/Tools/induct_tacs.ML Thu Mar 05 11:58:53 2009 +0100
52.2 +++ b/src/ZF/Tools/induct_tacs.ML Thu Mar 05 12:08:00 2009 +0100
52.3 @@ -157,7 +157,7 @@
52.4
52.5 in
52.6 thy
52.7 - |> Sign.add_path (Sign.base_name big_rec_name)
52.8 + |> Sign.add_path (NameSpace.base_name big_rec_name)
52.9 |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
52.10 |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
52.11 |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
53.1 --- a/src/ZF/Tools/inductive_package.ML Thu Mar 05 11:58:53 2009 +0100
53.2 +++ b/src/ZF/Tools/inductive_package.ML Thu Mar 05 12:08:00 2009 +0100
53.3 @@ -80,7 +80,7 @@
53.4 val rec_names = map (#1 o dest_Const) rec_hds
53.5 and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
53.6
53.7 - val rec_base_names = map Sign.base_name rec_names;
53.8 + val rec_base_names = map NameSpace.base_name rec_names;
53.9 val dummy = assert_all Syntax.is_identifier rec_base_names
53.10 (fn a => "Base name of recursive set not an identifier: " ^ a);
53.11
53.12 @@ -377,7 +377,7 @@
53.13 mutual recursion to invariably be a disjoint sum.*)
53.14 fun mk_predpair rec_tm =
53.15 let val rec_name = (#1 o dest_Const o head_of) rec_tm
53.16 - val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
53.17 + val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name,
53.18 elem_factors ---> FOLogic.oT)
53.19 val qconcl =
53.20 List.foldr FOLogic.mk_all
54.1 --- a/src/ZF/Tools/primrec_package.ML Thu Mar 05 11:58:53 2009 +0100
54.2 +++ b/src/ZF/Tools/primrec_package.ML Thu Mar 05 12:08:00 2009 +0100
54.3 @@ -139,7 +139,7 @@
54.4 (** make definition **)
54.5
54.6 (*the recursive argument*)
54.7 - val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
54.8 + val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
54.9 Ind_Syntax.iT)
54.10
54.11 val def_tm = Logic.mk_equals
54.12 @@ -153,7 +153,7 @@
54.13 writeln ("primrec def:\n" ^
54.14 Syntax.string_of_term_global thy def_tm)
54.15 else();
54.16 - (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
54.17 + (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
54.18 def_tm)
54.19 end;
54.20
54.21 @@ -168,7 +168,7 @@
54.22 val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
54.23
54.24 val ([def_thm], thy1) = thy
54.25 - |> Sign.add_path (Sign.base_name fname)
54.26 + |> Sign.add_path (NameSpace.base_name fname)
54.27 |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
54.28
54.29 val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)