# HG changeset patch
# User wenzelm
# Date 1236251280 -3600
# Node ID eb98b49ef835614063368c64a4fb490146fa05c9
# Parent  84097bba7bdc923f9a6174b28f9828485987a50e
renamed NameSpace.base to NameSpace.base_name;
renamed NameSpace.map_base to NameSpace.map_base_name;
eliminated alias Sign.base_name = NameSpace.base_name;

diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -72,7 +72,7 @@
  let 
    val thy = theory_of_thm thm;
 (* the parsing function returns a qualified name, we get back the base name *)
-   val atom_basename = Sign.base_name atom_name;
+   val atom_basename = NameSpace.base_name atom_name;
    val goal = List.nth(prems_of thm, i-1);
    val ps = Logic.strip_params goal;
    val Ts = rev (map snd ps);
@@ -159,7 +159,7 @@
     NONE => all_tac thm
   | SOME atom_name  =>    
   let 
-    val atom_basename = Sign.base_name atom_name;
+    val atom_basename = NameSpace.base_name atom_name;
     val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
     val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
     fun inst_fresh vars params i st =
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -199,7 +199,7 @@
     val atomTs = distinct op = (maps (map snd o #2) prems);
     val ind_sort = if null atomTs then HOLogic.typeS
       else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
-        ("fs_" ^ Sign.base_name (fst (dest_Type T)))) atomTs);
+        ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs);
     val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -273,7 +273,7 @@
 
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn aT => PureThy.get_thm thy
-      ("pt_" ^ Sign.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
+      ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
     val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
@@ -281,7 +281,7 @@
     val fresh_bij = PureThy.get_thms thy "fresh_bij";
     val perm_bij = PureThy.get_thms thy "perm_bij";
     val fs_atoms = map (fn aT => PureThy.get_thm thy
-      ("fs_" ^ Sign.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
+      ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
     val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
     val fresh_atm = PureThy.get_thms thy "fresh_atm";
     val swap_simps = PureThy.get_thms thy "swap_simps";
@@ -545,7 +545,7 @@
     ctxt'' |>
     Proof.theorem_i NONE (fn thss => fn ctxt =>
       let
-        val rec_name = space_implode "_" (map Sign.base_name names);
+        val rec_name = space_implode "_" (map NameSpace.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = RuleCases.case_names induct_cases;
         val induct_cases' = InductivePackage.partition_rules' raw_induct
@@ -575,7 +575,7 @@
              Attrib.internal (K (RuleCases.consumes 1))]),
            strong_inducts) |> snd |>
         LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
-            ((Binding.name (NameSpace.qualified (Sign.base_name name) "strong_cases"),
+            ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"),
               [Attrib.internal (K (RuleCases.case_names (map snd cases))),
                Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
           (strong_cases ~~ induct_cases')) |> snd
@@ -665,7 +665,7 @@
   in
     ctxt |>
     LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
-        ((Binding.name (NameSpace.qualified (Sign.base_name name) "eqvt"),
+        ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"),
           [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
       (names ~~ transp thss)) |> snd
   end;
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -229,7 +229,7 @@
     val atoms = map (fst o dest_Type) atomTs;
     val ind_sort = if null atomTs then HOLogic.typeS
       else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
-        ("fs_" ^ Sign.base_name a)) atoms);
+        ("fs_" ^ NameSpace.base_name a)) atoms);
     val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
     val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
     val fsT = TFree (fs_ctxt_tyname, ind_sort);
@@ -296,7 +296,7 @@
 
     val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
     val pt2_atoms = map (fn a => PureThy.get_thm thy
-      ("pt_" ^ Sign.base_name a ^ "2")) atoms;
+      ("pt_" ^ NameSpace.base_name a ^ "2")) atoms;
     val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
       addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
       addsimprocs [mk_perm_bool_simproc ["Fun.id"],
@@ -324,7 +324,7 @@
         val atom = fst (dest_Type T);
         val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
         val fs_atom = PureThy.get_thm thy
-          ("fs_" ^ Sign.base_name atom ^ "1");
+          ("fs_" ^ NameSpace.base_name atom ^ "1");
         val avoid_th = Drule.instantiate'
           [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
           ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
@@ -452,7 +452,7 @@
     ctxt'' |>
     Proof.theorem_i NONE (fn thss => fn ctxt =>
       let
-        val rec_name = space_implode "_" (map Sign.base_name names);
+        val rec_name = space_implode "_" (map NameSpace.base_name names);
         val rec_qualified = Binding.qualify false rec_name;
         val ind_case_names = RuleCases.case_names induct_cases;
         val induct_cases' = InductivePackage.partition_rules' raw_induct
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -49,9 +49,9 @@
 
 fun dt_cases (descr: descr) (_, args, constrs) =
   let
-    fun the_bname i = Sign.base_name (#1 (valOf (AList.lookup (op =) descr i)));
+    fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
-  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
+  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
 
 
 fun induct_cases descr =
@@ -364,7 +364,7 @@
         val pi2 = Free ("pi2", permT);
         val pt_inst = pt_inst_of thy2 a;
         val pt2' = pt_inst RS pt2;
-        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "2") a);
+        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a);
       in List.take (map standard (split_conj_thm
         (Goal.prove_global thy2 [] []
            (augment_sort thy2 [pt_class_of thy2 a]
@@ -399,7 +399,7 @@
         val pt_inst = pt_inst_of thy2 a;
         val pt3' = pt_inst RS pt3;
         val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
-        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base (fn s => "pt_" ^ s ^ "3") a);
+        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a);
       in List.take (map standard (split_conj_thm
         (Goal.prove_global thy2 [] []
           (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
@@ -664,7 +664,7 @@
               asm_full_simp_tac (simpset_of thy addsimps
                 [Rep RS perm_closed RS Abs_inverse]) 1,
               asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
-                ("pt_" ^ Sign.base_name atom ^ "3")]) 1]) thy
+                ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy
           end)
         (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
            new_type_names ~~ tyvars ~~ perm_closed_thms);
@@ -798,7 +798,7 @@
         val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> T') $ lhs, rhs));
-        val def_name = (Sign.base_name cname) ^ "_def";
+        val def_name = (NameSpace.base_name cname) ^ "_def";
         val ([def_thm], thy') = thy |>
           Sign.add_consts_i [(cname', constrT, mx)] |>
           (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
@@ -889,7 +889,7 @@
           map (fn ((cname, dts), constr_rep_thm) =>
         let
           val cname = Sign.intern_const thy8
-            (NameSpace.append tname (Sign.base_name cname));
+            (NameSpace.append tname (NameSpace.base_name cname));
           val permT = mk_permT (Type (atom, []));
           val pi = Free ("pi", permT);
 
@@ -945,7 +945,7 @@
         if null dts then NONE else SOME
         let
           val cname = Sign.intern_const thy8
-            (NameSpace.append tname (Sign.base_name cname));
+            (NameSpace.append tname (NameSpace.base_name cname));
 
           fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
             let
@@ -987,7 +987,7 @@
       in List.concat (map (fn (cname, dts) => map (fn atom =>
         let
           val cname = Sign.intern_const thy8
-            (NameSpace.append tname (Sign.base_name cname));
+            (NameSpace.append tname (NameSpace.base_name cname));
           val atomT = Type (atom, []);
 
           fun process_constr ((dts, dt), (j, args1, args2)) =
@@ -1100,7 +1100,7 @@
            (fn _ => indtac dt_induct indnames 1 THEN
             ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
               (abs_supp @ supp_atm @
-               PureThy.get_thms thy8 ("fs_" ^ Sign.base_name atom ^ "1") @
+               PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @
                List.concat supp_thms))))),
          length new_type_names))
       end) atoms;
@@ -1232,9 +1232,9 @@
     val fin_set_fresh = map (fn s =>
       at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
     val pt1_atoms = map (fn Type (s, _) =>
-      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "1")) dt_atomTs;
+      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs;
     val pt2_atoms = map (fn Type (s, _) =>
-      PureThy.get_thm thy9 ("pt_" ^ Sign.base_name s ^ "2") RS sym) dt_atomTs;
+      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs;
     val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
     val fs_atoms = PureThy.get_thms thy9 "fin_supp";
     val abs_supp = PureThy.get_thms thy9 "abs_supp";
@@ -1559,7 +1559,7 @@
 
     val rec_fin_supp_thms = map (fn aT =>
       let
-        val name = Sign.base_name (fst (dest_Type aT));
+        val name = NameSpace.base_name (fst (dest_Type aT));
         val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
         val aset = HOLogic.mk_setT aT;
         val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
@@ -1598,7 +1598,7 @@
 
     val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
       let
-        val name = Sign.base_name (fst (dest_Type aT));
+        val name = NameSpace.base_name (fst (dest_Type aT));
         val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
         val a = Free ("a", aT);
         val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
@@ -2012,10 +2012,10 @@
     val (reccomb_defs, thy12) =
       thy11
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
-          (Sign.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
+          (NameSpace.base_name name, rec_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
-          (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
+          (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_permeq.ML
--- a/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -110,7 +110,7 @@
           Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
             (if (applicable_app f) then
               let
-                val name = Sign.base_name n
+                val name = NameSpace.base_name n
                 val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
                 val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
               in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
@@ -198,8 +198,8 @@
          Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
           pi2 $ t)) =>
     let
-      val tname' = Sign.base_name tname
-      val uname' = Sign.base_name uname
+      val tname' = NameSpace.base_name tname
+      val uname' = NameSpace.base_name uname
     in
       if pi1 <> pi2 then  (* only apply the composition rule in this case *)
         if T = U then    
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -207,7 +207,7 @@
     val frees = ls @ x :: rs;
     val raw_rhs = list_abs_free (frees,
       list_comb (Const (rec_name, dummyT), fs @ [Free x]))
-    val def_name = Thm.def_name (Sign.base_name fname);
+    val def_name = Thm.def_name (NameSpace.base_name fname);
     val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     val SOME var = get_first (fn ((b, _), mx) =>
       if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
@@ -286,7 +286,7 @@
       fold_map (apfst (snd o snd) oo
         LocalTheory.define Thm.definitionK o fst) defs';
     val qualify = Binding.qualify false
-      (space_implode "_" (map (Sign.base_name o #1) defs));
+      (space_implode "_" (map (NameSpace.base_name o #1) defs));
     val names_atts' = map (apfst qualify) names_atts;
     val cert = cterm_of (ProofContext.theory_of lthy');
 
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -115,7 +115,7 @@
                (Var (n,ty))) =>
              let
                 (* FIXME: this should be an operation the library *)
-                val class_name = (NameSpace.map_base (fn s => "pt_"^s) tyatm)
+                val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
              in
                 if (Sign.of_sort thy (ty,[class_name]))
                 then [(pi,typi)]
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -336,17 +336,17 @@
     [] => ""
    | c::cs => String.implode (Char.toUpper c::cs ))
 
-fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base T)
-  | mkName (TFree (x,_)) = mkUpper (NameSpace.base x)
-  | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base x);
+fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T)
+  | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x)
+  | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x);
 
 fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
 
-fun mk_map ("List.list") = Syntax.const "List.map"
-  | mk_map n = Syntax.const ("StateFun." ^  "map_" ^ NameSpace.base n);
+fun mk_map "List.list" = Syntax.const "List.map"
+  | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n);
 
 fun gen_constr_destr comp prfx thy (Type (T,[])) = 
-      Syntax.const (deco prfx (mkUpper (NameSpace.base T)))
+      Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))
   | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
      let val (argTs,rangeT) = strip_type T;
      in comp 
@@ -360,11 +360,11 @@
      then (* datatype args are recursively embedded into val *)
          (case argTs of
            [argT] => comp 
-                     ((Syntax.const (deco prfx (mkUpper (NameSpace.base T)))))
+                     ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))))
                      ((mk_map T $ gen_constr_destr comp prfx thy argT))
           | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
      else (* type args are not recursively embedded into val *)
-           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base T)))
+           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T)))
   | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
                    
 val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -645,7 +645,7 @@
 fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
 
 fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
-     if NameSpace.base k = NameSpace.base KN then
+     if NameSpace.base_name k = NameSpace.base_name KN then
         (case get_comp (Context.Proof ctxt) name of
           SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
                            Syntax.const "_statespace_update" $ s $ n $ v
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -223,7 +223,7 @@
  *---------------------------------------------------------------------------*)
 fun define_i strict thy cs ss congs wfs fid R eqs =
   let val {functional,pats} = Prim.mk_functional thy eqs
-      val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
+      val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional
       val {induct, rules, tcs} = 
           simplify_defn strict thy cs ss congs wfs fid pats def
       val rules' = 
@@ -248,7 +248,7 @@
 
 fun defer_i thy congs fid eqs =
  let val {rules,R,theory,full_pats_TCs,SV,...} =
-             Prim.lazyR_def thy (Sign.base_name fid) congs eqs
+             Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs
      val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
      val dummy = writeln "Proving induction theorem ...";
      val induction = Prim.mk_induction theory
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/TFL/tfl.ML
--- a/src/HOL/Tools/TFL/tfl.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/TFL/tfl.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -349,7 +349,7 @@
           | L => mk_functional_err
  ("The following clauses are redundant (covered by preceding clauses): " ^
                    commas (map (fn i => Int.toString (i + 1)) L))
- in {functional = Abs(Sign.base_name fname, ftype,
+ in {functional = Abs(NameSpace.base_name fname, ftype,
                       abstract_over (atom,
                                      absfree(aname,atype, case_tm))),
      pats = patts2}
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -235,10 +235,10 @@
     val (reccomb_defs, thy2) =
       thy1
       |> Sign.add_consts_i (map (fn ((name, T), T') =>
-          (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
+          (NameSpace.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
           (reccomb_names ~~ recTs ~~ rec_result_Ts))
       |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
-          (Binding.name (Sign.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
+          (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
            Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
              set $ Free ("x", T) $ Free ("y", T'))))))
                (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
@@ -316,8 +316,8 @@
           val fns = (List.concat (Library.take (i, case_dummy_fns))) @
             fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
           val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
-          val decl = ((Binding.name (Sign.base_name name), caseT), NoSyn);
-          val def = (Binding.name (Sign.base_name name ^ "_def"),
+          val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn);
+          val def = (Binding.name (NameSpace.base_name name ^ "_def"),
             Logic.mk_equals (list_comb (Const (name, caseT), fns1),
               list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
                 fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -224,7 +224,7 @@
   | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
 
 fun name_of_typ (Type (s, Ts)) =
-      let val s' = Sign.base_name s
+      let val s' = NameSpace.base_name s
       in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
         [if Syntax.is_identifier s' then s' else "x"])
       end
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -174,9 +174,9 @@
 
 fun dt_cases (descr: descr) (_, args, constrs) =
   let
-    fun the_bname i = Sign.base_name (#1 (the (AList.lookup (op =) descr i)));
+    fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
     val bnames = map the_bname (distinct (op =) (maps dt_recs args));
-  in map (fn (c, _) => space_implode "_" (Sign.base_name c :: bnames)) constrs end;
+  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
 
 
 fun induct_cases descr =
@@ -519,7 +519,7 @@
     val cs = map (apsnd (map norm_constr)) raw_cs;
     val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
       o fst o strip_type;
-    val new_type_names = map NameSpace.base (the_default (map fst cs) alt_names);
+    val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
 
     fun mk_spec (i, (tyco, constr)) = (i, (tyco,
       map (DtTFree o fst) vs,
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_prop.ML
--- a/src/HOL/Tools/datatype_prop.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_prop.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -47,7 +47,7 @@
   let
     fun type_name (TFree (name, _)) = implode (tl (explode name))
       | type_name (Type (name, _)) = 
-          let val name' = Sign.base_name name
+          let val name' = NameSpace.base_name name
           in if Syntax.is_identifier name' then name' else "x" end;
   in indexify_names (map type_name Ts) end;
 
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -168,7 +168,7 @@
         val Ts = map (typ_of_dtyp descr sorts) cargs;
         val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
-        val r = Free ("r" ^ NameSpace.base cname, Ts ---> rT)
+        val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
       in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
         (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
           HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/datatype_rep_proofs.ML
--- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -236,7 +236,7 @@
         val lhs = list_comb (Const (cname, constrT), l_args);
         val rhs = mk_univ_inj r_args n i;
         val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
-        val def_name = Sign.base_name cname ^ "_def";
+        val def_name = NameSpace.base_name cname ^ "_def";
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
         val ([def_thm], thy') =
@@ -343,7 +343,7 @@
         
         val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
         val fTs = map fastype_of fs;
-        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Sign.base_name iso_name ^ "_def"),
+        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"),
           Logic.mk_equals (Const (iso_name, T --> Univ_elT),
             list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
         val (def_thms, thy') =
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/function_package/size.ML
--- a/src/HOL/Tools/function_package/size.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/function_package/size.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -87,7 +87,7 @@
       recTs1 ~~ alt_names' |>
       map (fn (T as Type (s, _), optname) =>
         let
-          val s' = the_default (Sign.base_name s) optname ^ "_size";
+          val s' = the_default (NameSpace.base_name s) optname ^ "_size";
           val s'' = Sign.full_bname thy s'
         in
           (s'',
@@ -140,7 +140,7 @@
     val ((size_def_thms, size_def_thms'), thy') =
       thy
       |> Sign.add_consts_i (map (fn (s, T) =>
-           (Sign.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
+           (NameSpace.base_name s, param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
            (size_names ~~ recTs1))
       |> PureThy.add_defs false
         (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
@@ -221,8 +221,8 @@
 fun add_size_thms (new_type_names as name :: _) thy =
   let
     val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
-    val prefix = NameSpace.map_base (K (space_implode "_"
-      (the_default (map Sign.base_name new_type_names) alt_names))) name;
+    val prefix = NameSpace.map_base_name (K (space_implode "_"
+      (the_default (map NameSpace.base_name new_type_names) alt_names))) name;
     val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
       is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
   in if no_size then thy
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -698,7 +698,7 @@
       ctxt1 |>
       LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
       fold_map (fn (name, (elim, cases)) =>
-        LocalTheory.note kind ((Binding.name (NameSpace.qualified (Sign.base_name name) "cases"),
+        LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
           [Attrib.internal (K (RuleCases.case_names cases)),
            Attrib.internal (K (RuleCases.consumes 1)),
            Attrib.internal (K (Induct.cases_pred name)),
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -68,8 +68,8 @@
     val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (prop_of (hd intrs))));
     val params = map dest_Var (Library.take (nparms, ts));
-    val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
-    fun constr_of_intr intr = (Sign.base_name (name_of_thm intr),
+    val tname = space_implode "_" (NameSpace.base_name s ^ "T" :: vs);
+    fun constr_of_intr intr = (NameSpace.base_name (name_of_thm intr),
       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -112,7 +112,7 @@
     val rT = if n then Extraction.nullT
       else Type (space_implode "_" (s ^ "T" :: vs),
         map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
-    val r = if n then Extraction.nullt else Var ((Sign.base_name s, 0), rT);
+    val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT);
     val S = list_comb (h, params @ xs);
     val rvs = relevant_vars S;
     val vs' = map fst rvs \\ vs;
@@ -195,7 +195,7 @@
           in if conclT = Extraction.nullT
             then list_abs_free (map dest_Free xs, HOLogic.unit)
             else list_abs_free (map dest_Free xs, list_comb
-              (Free ("r" ^ Sign.base_name (name_of_thm intr),
+              (Free ("r" ^ NameSpace.base_name (name_of_thm intr),
                 map fastype_of (rev args) ---> conclT), rev args))
           end
 
@@ -217,7 +217,7 @@
       end) (premss ~~ dummies);
     val frees = fold Term.add_frees fs [];
     val Ts = map fastype_of fs;
-    fun name_of_fn intr = "r" ^ Sign.base_name (name_of_thm intr)
+    fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr)
   in
     fst (fold_map (fn concl => fn names =>
       let val T = Extraction.etype_of thy vs [] concl
@@ -245,7 +245,7 @@
       |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
     handle DatatypeAux.Datatype_Empty name' =>
       let
-        val name = Sign.base_name name';
+        val name = NameSpace.base_name name';
         val dname = Name.variant used "Dummy"
       in
         thy
@@ -296,7 +296,7 @@
 
     val thy1' = thy1 |>
       Theory.copy |>
-      Sign.add_types (map (fn s => (Sign.base_name s, ar, NoSyn)) tnames) |>
+      Sign.add_types (map (fn s => (NameSpace.base_name s, ar, NoSyn)) tnames) |>
       fold (fn s => AxClass.axiomatize_arity
         (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
         Extraction.add_typeof_eqns_i ty_eqs;
@@ -335,7 +335,7 @@
         let
           val Const (s, T) = head_of (HOLogic.dest_Trueprop
             (Logic.strip_assums_concl rintr));
-          val s' = Sign.base_name s;
+          val s' = NameSpace.base_name s;
           val T' = Logic.unvarifyT T
         in (((Binding.name s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) rintrs));
     val rlzparams = map (fn Var ((s, _), T) => (s, Logic.unvarifyT T))
@@ -349,7 +349,7 @@
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
           coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
-          ((Binding.name (Sign.base_name (name_of_thm intr)), []),
+          ((Binding.name (NameSpace.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))
              (rintrs ~~ maps snd rss)) [] ||>
       Sign.absolute_path;
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/old_primrec_package.ML
--- a/src/HOL/Tools/old_primrec_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/old_primrec_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -212,7 +212,7 @@
                     ((map snd ls) @ [dummyT])
                     (list_comb (Const (rec_name, dummyT),
                                 fs @ map Bound (0 ::(length ls downto 1))))
-    val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
+    val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
     val def_prop =
       singleton (Syntax.check_terms (ProofContext.init thy))
         (Logic.mk_equals (Const (fname, dummyT), rhs));
@@ -269,7 +269,7 @@
             else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
               "\nare not mutually recursive");
     val primrec_name =
-      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
+      if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
     val (defs_thms', thy') =
       thy
       |> Sign.add_path primrec_name
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/primrec_package.ML
--- a/src/HOL/Tools/primrec_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/primrec_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -191,7 +191,7 @@
                     (map snd ls @ [dummyT])
                     (list_comb (Const (rec_name, dummyT),
                                 fs @ map Bound (0 :: (length ls downto 1))))
-    val def_name = Thm.def_name (Sign.base_name fname);
+    val def_name = Thm.def_name (NameSpace.base_name fname);
     val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
     val SOME var = get_first (fn ((b, _), mx) =>
       if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
@@ -247,7 +247,7 @@
     val _ = if gen_eq_set (op =) (names1, names2) then ()
       else primrec_error ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
-    val prefix = space_implode "_" (map (Sign.base_name o #1) defs);
+    val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs);
     val qualify = Binding.qualify false prefix;
     val spec' = (map o apfst)
       (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -193,7 +193,7 @@
     val _ = requires_recdef thy;
 
     val name = Sign.intern_const thy raw_name;
-    val bname = Sign.base_name name;
+    val bname = NameSpace.base_name name;
     val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
 
     val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
@@ -233,7 +233,7 @@
 fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
   let
     val name = Sign.intern_const thy raw_name;
-    val bname = Sign.base_name name;
+    val bname = NameSpace.base_name name;
 
     val _ = requires_recdef thy;
     val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -122,7 +122,7 @@
 (* syntax *)
 
 fun prune n xs = Library.drop (n, xs);
-fun prefix_base s = NameSpace.map_base (fn bname => s ^ bname);
+fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname);
 
 val Trueprop = HOLogic.mk_Trueprop;
 fun All xs t = Term.list_all_free (xs, t);
@@ -702,7 +702,7 @@
                      SOME flds
                      => (let
                           val (f::fs) = but_last (map fst flds);
-                          val flds' = Sign.extern_const thy f :: map NameSpace.base fs;
+                          val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs;
                           val (args',more) = split_last args;
                          in (flds'~~args')@field_lst more end
                          handle Library.UnequalLengths => [("",t)])
@@ -804,7 +804,7 @@
                            => (let
                                 val (f :: fs) = but_last flds;
                                 val flds' = apfst (Sign.extern_const thy) f
-                                  :: map (apfst NameSpace.base) fs;
+                                  :: map (apfst NameSpace.base_name) fs;
                                 val (args', more) = split_last args;
                                 val alphavars = map varifyT (but_last alphas);
                                 val subst = fold2 (curry (Sign.typ_match thy))
@@ -1069,7 +1069,7 @@
              val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
 
              (*fun mk_abs_var x t = (x, fastype_of t);*)
-             fun sel_name u = NameSpace.base (unsuffix updateN u);
+             fun sel_name u = NameSpace.base_name (unsuffix updateN u);
 
              fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
                   if has_field extfields s (domain_type' mT) then upd else seed s r
@@ -1463,7 +1463,7 @@
       in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
   in
     thy
-    |> TypecopyPackage.add_typecopy (suffix ext_typeN (Sign.base_name name), alphas) repT NONE
+    |> TypecopyPackage.add_typecopy (suffix ext_typeN (NameSpace.base_name name), alphas) repT NONE
     |-> (fn (name, _) => `(fn thy => get_thms thy name))
   end;
 
@@ -1474,7 +1474,7 @@
 
 fun extension_definition full name fields names alphas zeta moreT more vars thy =
   let
-    val base = Sign.base_name;
+    val base = NameSpace.base_name;
     val fieldTs = (map snd fields);
     val alphas_zeta = alphas@[zeta];
     val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
@@ -1760,7 +1760,7 @@
     val alphas = map fst args;
     val name = Sign.full_bname thy bname;
     val full = Sign.full_bname_path thy bname;
-    val base = Sign.base_name;
+    val base = NameSpace.base_name;
 
     val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
 
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -380,7 +380,7 @@
 
 (*Ignore blacklisted basenames*)
 fun add_multi_names ((a, ths), pairs) =
-  if (Sign.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
+  if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   else add_single_names ((a, ths), pairs);
 
 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -342,7 +342,7 @@
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
 fun skolem_thm (s, th) =
-  if member (op =) multi_base_blacklist (Sign.base_name s) orelse bad_for_atp th then []
+  if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
   else
     let
       val ctxt0 = Variable.thm_context th
@@ -444,7 +444,7 @@
     val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
       if already_seen thy name then I else cons (name, ths));
     val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
-      if member (op =) multi_base_blacklist (Sign.base_name name) then I
+      if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
       else fold_index (fn (i, th) =>
         if bad_for_atp th orelse is_some (lookup_cache thy th) then I
         else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/Tools/specification_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -24,7 +24,7 @@
                 val ctype = domain_type (type_of P)
                 val cname_full = Sign.intern_const thy cname
                 val cdefname = if thname = ""
-                               then Thm.def_name (Sign.base_name cname)
+                               then Thm.def_name (NameSpace.base_name cname)
                                else thname
                 val def_eq = Logic.mk_equals (Const(cname_full,ctype),
                                               HOLogic.choice_const ctype $  P)
@@ -50,7 +50,7 @@
                         val ctype = domain_type (type_of P)
                         val cname_full = Sign.intern_const thy cname
                         val cdefname = if thname = ""
-                                       then Thm.def_name (Sign.base_name cname)
+                                       then Thm.def_name (NameSpace.base_name cname)
                                        else thname
                         val co = Const(cname_full,ctype)
                         val thy' = Theory.add_finals_i covld [co] thy
@@ -154,7 +154,7 @@
         fun mk_exist (c,prop) =
             let
                 val T = type_of c
-                val cname = Sign.base_name (fst (dest_Const c))
+                val cname = NameSpace.base_name (fst (dest_Const c))
                 val vname = if Syntax.is_identifier cname
                             then cname
                             else "x"
diff -r 84097bba7bdc -r eb98b49ef835 src/HOL/ex/Quickcheck_Generators.thy
--- a/src/HOL/ex/Quickcheck_Generators.thy	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOL/ex/Quickcheck_Generators.thy	Thu Mar 05 12:08:00 2009 +0100
@@ -138,7 +138,7 @@
     let
       val this_ty = Type (hd tycos, map TFree vs);
       val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
-      val random_name = NameSpace.base @{const_name random};
+      val random_name = NameSpace.base_name @{const_name random};
       val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
       fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
       val random' = Free (random'_name,
diff -r 84097bba7bdc -r eb98b49ef835 src/HOLCF/Tools/domain/domain_axioms.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -22,7 +22,7 @@
   val dc_rep = %%:(dname^"_rep");
   val x_name'= "x";
   val x_name = idx_name eqs x_name' (n+1);
-  val dnam = Sign.base_name dname;
+  val dnam = NameSpace.base_name dname;
 
   val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
   val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
diff -r 84097bba7bdc -r eb98b49ef835 src/HOLCF/Tools/domain/domain_extender.ML
--- a/src/HOLCF/Tools/domain/domain_extender.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_extender.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -103,7 +103,7 @@
 			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
-    fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
+    fun thy_type  (dname,tvars)  = (NameSpace.base_name dname, length tvars, NoSyn);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
 		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
@@ -114,7 +114,7 @@
     val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
     fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
     fun typid (Type  (id,_)) =
-          let val c = hd (Symbol.explode (Sign.base_name id))
+          let val c = hd (Symbol.explode (NameSpace.base_name id))
           in if Symbol.is_letter c then c else "t" end
       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
@@ -133,7 +133,7 @@
       ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   in
     theorems_thy
-    |> Sign.add_path (Sign.base_name comp_dnam)
+    |> Sign.add_path (NameSpace.base_name comp_dnam)
     |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
     |> Sign.parent_path
   end;
diff -r 84097bba7bdc -r eb98b49ef835 src/HOLCF/Tools/domain/domain_syntax.ML
--- a/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -25,7 +25,7 @@
 in
   val dtype  = Type(dname,typevars);
   val dtype2 = foldr1 mk_ssumT (map prod cons');
-  val dnam = Sign.base_name dname;
+  val dnam = NameSpace.base_name dname;
   val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
diff -r 84097bba7bdc -r eb98b49ef835 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -606,7 +606,7 @@
 
 in
   thy
-    |> Sign.add_path (Sign.base_name dname)
+    |> Sign.add_path (NameSpace.base_name dname)
     |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
         ("iso_rews" , iso_rews  ),
         ("exhaust"  , [exhaust] ),
diff -r 84097bba7bdc -r eb98b49ef835 src/HOLCF/Tools/fixrec_package.ML
--- a/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/HOLCF/Tools/fixrec_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -181,7 +181,7 @@
     val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
     
     fun one_def (l as Free(n,_)) r =
-          let val b = Sign.base_name n
+          let val b = NameSpace.base_name n
           in ((Binding.name (b^"_def"), []), r) end
       | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
     fun defs [] _ = []
@@ -230,7 +230,7 @@
 
 fun taken_names (t : term) : bstring list =
   let
-    fun taken (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
+    fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
       | taken (Free(a,_) , bs) = insert (op =) a bs
       | taken (f $ u     , bs) = taken (f, taken (u, bs))
       | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -25,9 +25,9 @@
   val explode: string -> string list
   val append: string -> string -> string
   val qualified: string -> string -> string
-  val base: string -> string
+  val base_name: string -> string
   val qualifier: string -> string
-  val map_base: (string -> string) -> string -> string
+  val map_base_name: (string -> string) -> string -> string
   type T
   val empty: T
   val intern: T -> xstring -> string
@@ -78,14 +78,14 @@
   if path = "" orelse name = "" then name
   else path ^ separator ^ name;
 
-fun base "" = ""
-  | base name = List.last (explode_name name);
+fun base_name "" = ""
+  | base_name name = List.last (explode_name name);
 
 fun qualifier "" = ""
   | qualifier name = implode_name (#1 (split_last (explode_name name)));
 
-fun map_base _ "" = ""
-  | map_base f name =
+fun map_base_name _ "" = ""
+  | map_base_name f name =
       let val names = explode_name name
       in implode_name (nth_map (length names - 1) f names) end;
 
@@ -161,7 +161,7 @@
       | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
   in
     if long_names then name
-    else if short_names then base name
+    else if short_names then base_name name
     else ext (get_accesses space name)
   end;
 
@@ -204,7 +204,7 @@
     let val names = valid_accesses space name in
       space
       |> add_name' name name
-      |> fold (del_name name) (if fully then names else names inter_string [base name])
+      |> fold (del_name name) (if fully then names else names inter_string [base_name name])
       |> fold (del_name_extra name) (get_accesses space name)
     end;
 
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -300,7 +300,7 @@
   map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
 
 fun redeclare_const thy c =
-  let val b = Sign.base_name c
+  let val b = NameSpace.base_name c
   in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
 
 fun synchronize_class_syntax sort base_sort ctxt =
@@ -358,7 +358,7 @@
 
 (* class target *)
 
-val class_prefix = Logic.const_of_class o Sign.base_name;
+val class_prefix = Logic.const_of_class o NameSpace.base_name;
 
 fun declare class pos ((c, mx), dict) thy =
   let
@@ -475,7 +475,7 @@
 
 fun type_name "*" = "prod"
   | type_name "+" = "sum"
-  | type_name s = sanatize_name (NameSpace.base s);
+  | type_name s = sanatize_name (NameSpace.base_name s);
 
 fun resort_terms pp algebra consts constraints ts =
   let
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/Isar/element.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -202,7 +202,7 @@
   let val head =
     if Thm.has_name_hint th then
       Pretty.block [Pretty.command kind,
-        Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
+        Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")]
     else Pretty.command kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/Isar/proof_display.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -75,7 +75,7 @@
 
 fun pretty_fact_name (kind, "") = Pretty.str kind
   | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
-      Pretty.str (NameSpace.base name), Pretty.str ":"];
+      Pretty.str (NameSpace.base_name name), Pretty.str ":"];
 
 fun pretty_facts ctxt =
   flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -330,7 +330,7 @@
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   Data.put ta #>
-  LocalTheory.init (NameSpace.base target)
+  LocalTheory.init (NameSpace.base_name target)
    {pretty = pretty ta,
     abbrev = abbrev ta,
     define = define ta,
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -110,7 +110,7 @@
 
 fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
     #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
-    |> syn ? Sign.base_name
+    |> syn ? NameSpace.base_name
     |> ML_Syntax.print_string));
 
 val _ = inline "type_name" (type_ false);
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -33,7 +33,7 @@
                | _ => ["global"]);
             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
             val entry =
-              {name = Sign.base_name name,
+              {name = NameSpace.base_name name,
                ID = name,
                dir = space_implode "/" (session @ prefix),
                unfold = false,
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/axclass.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -158,7 +158,7 @@
 
 (* maintain instances *)
 
-fun instance_name (a, c) = NameSpace.base c ^ "_" ^ NameSpace.base a;
+fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a;
 
 val get_instances = #1 o #2 o AxClassData.get;
 val map_instances = AxClassData.map o apsnd o apfst;
@@ -367,7 +367,7 @@
       | NONE => error ("Illegal type for instantiation of class parameter: "
         ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
     val name_inst = instance_name (tyco, class) ^ "_inst";
-    val c' = NameSpace.base c ^ "_" ^ NameSpace.base tyco;
+    val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
     val T' = Type.strip_sorts T;
   in
     thy
@@ -391,7 +391,7 @@
     val (c', eq) = get_inst_param thy (c, tyco);
     val prop = Logic.mk_equals (Const (c', T), t);
     val name' = Thm.def_name_optional
-      (NameSpace.base c ^ "_" ^ NameSpace.base tyco) name;
+      (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
   in
     thy
     |> Thm.add_def false false (Binding.name name', prop)
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/consts.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -120,7 +120,7 @@
 fun syntax consts (c, mx) =
   let
     val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
-    val c' = if authentic then Syntax.constN ^ c else NameSpace.base c;
+    val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c;
   in (c', T, mx) end;
 
 fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/logic.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -230,7 +230,7 @@
 (* class relations *)
 
 fun name_classrel (c1, c2) =
-  NameSpace.base c1 ^ "_" ^ NameSpace.base c2;
+  NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
 
 fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
 
@@ -243,8 +243,8 @@
 (* type arities *)
 
 fun name_arities (t, _, S) =
-  let val b = NameSpace.base t
-  in S |> map (fn c => NameSpace.base c ^ "_" ^ b) end;
+  let val b = NameSpace.base_name t
+  in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
 
 fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
 
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/old_term.ML
--- a/src/Pure/old_term.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/old_term.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -39,7 +39,7 @@
 
 (*Accumulates the names in the term, suppressing duplicates.
   Includes Frees and Consts.  For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
+fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
   | add_term_names (Free(a,_), bs) = insert (op =) a bs
   | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/primitive_defs.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -81,7 +81,7 @@
 fun mk_defpair (lhs, rhs) =
   (case Term.head_of lhs of
     Const (name, _) =>
-      (NameSpace.base name ^ "_def", Logic.mk_equals (lhs, rhs))
+      (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
   | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
 
 end;
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/sign.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -14,7 +14,6 @@
     consts: Consts.T}
   val naming_of: theory -> NameSpace.naming
   val full_name: theory -> binding -> string
-  val base_name: string -> bstring
   val full_bname: theory -> bstring -> string
   val full_bname_path: theory -> string -> bstring -> string
   val syn_of: theory -> Syntax.syntax
@@ -185,7 +184,6 @@
 (* naming *)
 
 val naming_of = #naming o rep_sg;
-val base_name = NameSpace.base;
 
 val full_name = NameSpace.full_name o naming_of;
 fun full_bname thy = NameSpace.full_name (naming_of thy) o Binding.name;
diff -r 84097bba7bdc -r eb98b49ef835 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Pure/term.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -490,7 +490,7 @@
 
 fun declare_term_names tm =
   fold_aterms
-    (fn Const (a, _) => Name.declare (NameSpace.base a)
+    (fn Const (a, _) => Name.declare (NameSpace.base_name a)
       | Free (a, _) => Name.declare a
       | _ => I) tm #>
   fold_types declare_typ_names tm;
@@ -721,7 +721,7 @@
 fun lambda v t =
   let val x =
     (case v of
-      Const (x, _) => NameSpace.base x
+      Const (x, _) => NameSpace.base_name x
     | Free (x, _) => x
     | Var ((x, _), _) => x
     | _ => Name.uu)
diff -r 84097bba7bdc -r eb98b49ef835 src/Tools/code/code_haskell.ML
--- a/src/Tools/code/code_haskell.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Tools/code/code_haskell.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -34,7 +34,7 @@
 fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
     init_syms deresolve is_cons contr_classparam_typs deriving_show =
   let
-    val deresolve_base = NameSpace.base o deresolve;
+    val deresolve_base = NameSpace.base_name o deresolve;
     fun class_name class = case syntax_class class
      of NONE => deresolve class
       | SOME class => class;
@@ -143,7 +143,7 @@
                 @ str "="
                 :: str "error"
                 @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
-                    o NameSpace.base o NameSpace.qualifier) name
+                    o NameSpace.base_name o NameSpace.qualifier) name
               )
             ]
           end
@@ -155,7 +155,7 @@
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
-                    then NONE else (SOME o NameSpace.base o deresolve) c)
+                    then NONE else (SOME o NameSpace.base_name o deresolve) c)
                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                 val vars = init_syms
                   |> Code_Name.intro_vars consts
@@ -255,7 +255,7 @@
                   let
                     val (c_inst_name, (_, tys)) = c_inst;
                     val const = if (is_some o syntax_const) c_inst_name
-                      then NONE else (SOME o NameSpace.base o deresolve) c_inst_name;
+                      then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name;
                     val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
                     val (vs, rhs) = unfold_abs_pure proto_rhs;
                     val vars = init_syms
@@ -360,7 +360,7 @@
     val reserved_names = Code_Name.make_vars reserved_names;
     fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
       syntax_class syntax_tyco syntax_const reserved_names
-      (if qualified then deresolver else NameSpace.base o deresolver)
+      (if qualified then deresolver else NameSpace.base_name o deresolver)
       is_cons contr_classparam_typs
       (if string_classes then deriving_show else K false);
     fun pr_module name content =
@@ -379,7 +379,7 @@
           |> map_filter (try deresolver);
         val qualified = is_none module_name andalso
           map deresolver stmt_names @ deps'
-          |> map NameSpace.base
+          |> map NameSpace.base_name
           |> has_duplicates (op =);
         val imports = deps'
           |> map NameSpace.qualifier
diff -r 84097bba7bdc -r eb98b49ef835 src/Tools/code/code_ml.ML
--- a/src/Tools/code/code_ml.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Tools/code/code_ml.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -47,7 +47,7 @@
   let
     val pr_label_classrel = translate_string (fn "." => "__" | c => c)
       o NameSpace.qualifier;
-    val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
+    val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier;
     fun pr_dicts fxy ds =
       let
         fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
@@ -163,7 +163,7 @@
     fun pr_stmt (MLExc (name, n)) =
           let
             val exc_str =
-              (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
+              (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
           in
             concat (
               str (if n = 0 then "val" else "fun")
@@ -179,7 +179,7 @@
           let
             val consts = map_filter
               (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o NameSpace.base o deresolve) c)
+                then NONE else (SOME o NameSpace.base_name o deresolve) c)
                 (Code_Thingol.fold_constnames (insert (op =)) t []);
             val vars = reserved_names
               |> Code_Name.intro_vars consts;
@@ -204,7 +204,7 @@
                   let
                     val consts = map_filter
                       (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o NameSpace.base o deresolve) c)
+                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                     val vars = reserved_names
                       |> Code_Name.intro_vars consts
@@ -473,7 +473,7 @@
     fun pr_stmt (MLExc (name, n)) =
           let
             val exc_str =
-              (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
+              (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
           in
             concat (
               str "let"
@@ -488,7 +488,7 @@
           let
             val consts = map_filter
               (fn c => if (is_some o syntax_const) c
-                then NONE else (SOME o NameSpace.base o deresolve) c)
+                then NONE else (SOME o NameSpace.base_name o deresolve) c)
                 (Code_Thingol.fold_constnames (insert (op =)) t []);
             val vars = reserved_names
               |> Code_Name.intro_vars consts;
@@ -508,7 +508,7 @@
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
-                    then NONE else (SOME o NameSpace.base o deresolve) c)
+                    then NONE else (SOME o NameSpace.base_name o deresolve) c)
                     ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                 val vars = reserved_names
                   |> Code_Name.intro_vars consts
@@ -524,7 +524,7 @@
                   let
                     val consts = map_filter
                       (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o NameSpace.base o deresolve) c)
+                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
                     val vars = reserved_names
                       |> Code_Name.intro_vars consts
@@ -552,7 +552,7 @@
                   let
                     val consts = map_filter
                       (fn c => if (is_some o syntax_const) c
-                        then NONE else (SOME o NameSpace.base o deresolve) c)
+                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
                         ((fold o Code_Thingol.fold_constnames)
                           (insert (op =)) (map (snd o fst) eqs) []);
                     val vars = reserved_names
diff -r 84097bba7bdc -r eb98b49ef835 src/Tools/code/code_thingol.ML
--- a/src/Tools/code/code_thingol.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/Tools/code/code_thingol.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -246,15 +246,15 @@
     in NameSpace.append prefix base end;
 in
 
-fun namify_class thy = namify thy NameSpace.base thyname_of_class;
+fun namify_class thy = namify thy NameSpace.base_name thyname_of_class;
 fun namify_classrel thy = namify thy (fn (class1, class2) => 
-  NameSpace.base class2 ^ "_" ^ NameSpace.base class1) (fn thy => thyname_of_class thy o fst);
+  NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst);
   (*order fits nicely with composed projections*)
 fun namify_tyco thy "fun" = "Pure.fun"
-  | namify_tyco thy tyco = namify thy NameSpace.base thyname_of_tyco tyco;
+  | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco;
 fun namify_instance thy = namify thy (fn (class, tyco) => 
-  NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
-fun namify_const thy = namify thy NameSpace.base thyname_of_const;
+  NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance;
+fun namify_const thy = namify thy NameSpace.base_name thyname_of_const;
 
 end; (* local *)
 
diff -r 84097bba7bdc -r eb98b49ef835 src/ZF/Tools/datatype_package.ML
--- a/src/ZF/Tools/datatype_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/datatype_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -74,7 +74,7 @@
                    Syntax.string_of_term_global thy t);
 
   val rec_names = map (#1 o dest_Const) rec_hds
-  val rec_base_names = map Sign.base_name rec_names
+  val rec_base_names = map NameSpace.base_name rec_names
   val big_rec_base_name = space_implode "_" rec_base_names
 
   val thy_path = thy |> Sign.add_path big_rec_base_name
diff -r 84097bba7bdc -r eb98b49ef835 src/ZF/Tools/induct_tacs.ML
--- a/src/ZF/Tools/induct_tacs.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -157,7 +157,7 @@
 
   in
     thy
-    |> Sign.add_path (Sign.base_name big_rec_name)
+    |> Sign.add_path (NameSpace.base_name big_rec_name)
     |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
     |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
     |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
diff -r 84097bba7bdc -r eb98b49ef835 src/ZF/Tools/inductive_package.ML
--- a/src/ZF/Tools/inductive_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/inductive_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -80,7 +80,7 @@
   val rec_names = map (#1 o dest_Const) rec_hds
   and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
 
-  val rec_base_names = map Sign.base_name rec_names;
+  val rec_base_names = map NameSpace.base_name rec_names;
   val dummy = assert_all Syntax.is_identifier rec_base_names
     (fn a => "Base name of recursive set not an identifier: " ^ a);
 
@@ -377,7 +377,7 @@
        mutual recursion to invariably be a disjoint sum.*)
      fun mk_predpair rec_tm =
        let val rec_name = (#1 o dest_Const o head_of) rec_tm
-           val pfree = Free(pred_name ^ "_" ^ Sign.base_name rec_name,
+           val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name,
                             elem_factors ---> FOLogic.oT)
            val qconcl =
              List.foldr FOLogic.mk_all
diff -r 84097bba7bdc -r eb98b49ef835 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Thu Mar 05 11:58:53 2009 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Thu Mar 05 12:08:00 2009 +0100
@@ -139,7 +139,7 @@
     (** make definition **)
 
     (*the recursive argument*)
-    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Sign.base_name big_rec_name),
+    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
                         Ind_Syntax.iT)
 
     val def_tm = Logic.mk_equals
@@ -153,7 +153,7 @@
             writeln ("primrec def:\n" ^
                      Syntax.string_of_term_global thy def_tm)
       else();
-      (Sign.base_name fname ^ "_" ^ Sign.base_name big_rec_name ^ "_def",
+      (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
        def_tm)
   end;
 
@@ -168,7 +168,7 @@
     val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
 
     val ([def_thm], thy1) = thy
-      |> Sign.add_path (Sign.base_name fname)
+      |> Sign.add_path (NameSpace.base_name fname)
       |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
 
     val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)