moved basic algebra of long names from structure NameSpace to Long_Name;
authorwenzelm
Sun Mar 08 17:26:14 2009 +0100 (2009-03-08)
changeset 30364577edc39b501
parent 30363 9b8d9b6ef803
child 30365 790129514c2d
moved basic algebra of long names from structure NameSpace to Long_Name;
src/HOL/Import/hol4rews.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_primrec.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_prop.ML
src/HOL/Tools/datatype_realizer.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/old_primrec_package.ML
src/HOL/Tools/primrec_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/record_package.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/specification_package.ML
src/HOL/ex/Quickcheck_Generators.thy
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_extender.ML
src/HOLCF/Tools/domain/domain_syntax.ML
src/HOLCF/Tools/domain/domain_theorems.ML
src/HOLCF/Tools/fixrec_package.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/element.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/theory_target.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Tools/find_theorems.ML
src/Pure/axclass.ML
src/Pure/codegen.ML
src/Pure/consts.ML
src/Pure/logic.ML
src/Pure/old_term.ML
src/Pure/primitive_defs.ML
src/Pure/sign.ML
src/Pure/term.ML
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_name.ML
src/Tools/code/code_thingol.ML
src/ZF/Tools/datatype_package.ML
src/ZF/Tools/induct_tacs.ML
src/ZF/Tools/inductive_package.ML
src/ZF/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Import/hol4rews.ML	Sun Mar 08 17:19:15 2009 +0100
     1.2 +++ b/src/HOL/Import/hol4rews.ML	Sun Mar 08 17:26:14 2009 +0100
     1.3 @@ -495,7 +495,7 @@
     1.4  	    if internal
     1.5  	    then
     1.6  		let
     1.7 -		    val paths = NameSpace.explode isa
     1.8 +		    val paths = Long_Name.explode isa
     1.9  		    val i = Library.drop(length paths - 2,paths)
    1.10  		in
    1.11  		    case i of
    1.12 @@ -549,10 +549,10 @@
    1.13  
    1.14  	fun gen2replay in_thy out_thy s = 
    1.15  	    let
    1.16 -		val ss = NameSpace.explode s
    1.17 +		val ss = Long_Name.explode s
    1.18  	    in
    1.19  		if (hd ss = in_thy) then 
    1.20 -		    NameSpace.implode (out_thy::(tl ss))
    1.21 +		    Long_Name.implode (out_thy::(tl ss))
    1.22  		else
    1.23  		    s
    1.24  	    end 
     2.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Mar 08 17:19:15 2009 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sun Mar 08 17:26:14 2009 +0100
     2.3 @@ -72,7 +72,7 @@
     2.4   let 
     2.5     val thy = theory_of_thm thm;
     2.6  (* the parsing function returns a qualified name, we get back the base name *)
     2.7 -   val atom_basename = NameSpace.base_name atom_name;
     2.8 +   val atom_basename = Long_Name.base_name atom_name;
     2.9     val goal = List.nth(prems_of thm, i-1);
    2.10     val ps = Logic.strip_params goal;
    2.11     val Ts = rev (map snd ps);
    2.12 @@ -159,7 +159,7 @@
    2.13      NONE => all_tac thm
    2.14    | SOME atom_name  =>    
    2.15    let 
    2.16 -    val atom_basename = NameSpace.base_name atom_name;
    2.17 +    val atom_basename = Long_Name.base_name atom_name;
    2.18      val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename;
    2.19      val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename;
    2.20      fun inst_fresh vars params i st =
     3.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Sun Mar 08 17:19:15 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Sun Mar 08 17:26:14 2009 +0100
     3.3 @@ -199,7 +199,7 @@
     3.4      val atomTs = distinct op = (maps (map snd o #2) prems);
     3.5      val ind_sort = if null atomTs then HOLogic.typeS
     3.6        else Sign.certify_sort thy (map (fn T => Sign.intern_class thy
     3.7 -        ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs);
     3.8 +        ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs);
     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 @@ -273,7 +273,7 @@
    3.13  
    3.14      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    3.15      val pt2_atoms = map (fn aT => PureThy.get_thm thy
    3.16 -      ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    3.17 +      ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs;
    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 @@ -281,7 +281,7 @@
    3.22      val fresh_bij = PureThy.get_thms thy "fresh_bij";
    3.23      val perm_bij = PureThy.get_thms thy "perm_bij";
    3.24      val fs_atoms = map (fn aT => PureThy.get_thm thy
    3.25 -      ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    3.26 +      ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs;
    3.27      val exists_fresh' = PureThy.get_thms thy "exists_fresh'";
    3.28      val fresh_atm = PureThy.get_thms thy "fresh_atm";
    3.29      val swap_simps = PureThy.get_thms thy "swap_simps";
    3.30 @@ -545,7 +545,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 NameSpace.base_name names);
    3.35 +        val rec_name = space_implode "_" (map Long_Name.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
    3.39 @@ -575,7 +575,7 @@
    3.40               Attrib.internal (K (RuleCases.consumes 1))]),
    3.41             strong_inducts) |> snd |>
    3.42          LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) =>
    3.43 -            ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"),
    3.44 +            ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"),
    3.45                [Attrib.internal (K (RuleCases.case_names (map snd cases))),
    3.46                 Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])]))
    3.47            (strong_cases ~~ induct_cases')) |> snd
    3.48 @@ -665,7 +665,7 @@
    3.49    in
    3.50      ctxt |>
    3.51      LocalTheory.notes Thm.theoremK (map (fn (name, ths) =>
    3.52 -        ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"),
    3.53 +        ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"),
    3.54            [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])]))
    3.55        (names ~~ transp thss)) |> snd
    3.56    end;
     4.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Sun Mar 08 17:19:15 2009 +0100
     4.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Sun Mar 08 17:26:14 2009 +0100
     4.3 @@ -229,7 +229,7 @@
     4.4      val atoms = map (fst o dest_Type) atomTs;
     4.5      val ind_sort = if null atomTs then HOLogic.typeS
     4.6        else Sign.certify_sort thy (map (fn a => Sign.intern_class thy
     4.7 -        ("fs_" ^ NameSpace.base_name a)) atoms);
     4.8 +        ("fs_" ^ Long_Name.base_name a)) atoms);
     4.9      val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt');
    4.10      val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt';
    4.11      val fsT = TFree (fs_ctxt_tyname, ind_sort);
    4.12 @@ -296,7 +296,7 @@
    4.13  
    4.14      val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp";
    4.15      val pt2_atoms = map (fn a => PureThy.get_thm thy
    4.16 -      ("pt_" ^ NameSpace.base_name a ^ "2")) atoms;
    4.17 +      ("pt_" ^ Long_Name.base_name a ^ "2")) atoms;
    4.18      val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss
    4.19        addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms)
    4.20        addsimprocs [mk_perm_bool_simproc ["Fun.id"],
    4.21 @@ -324,7 +324,7 @@
    4.22          val atom = fst (dest_Type T);
    4.23          val {at_inst, ...} = NominalAtoms.the_atom_info thy atom;
    4.24          val fs_atom = PureThy.get_thm thy
    4.25 -          ("fs_" ^ NameSpace.base_name atom ^ "1");
    4.26 +          ("fs_" ^ Long_Name.base_name atom ^ "1");
    4.27          val avoid_th = Drule.instantiate'
    4.28            [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)]
    4.29            ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding});
    4.30 @@ -452,7 +452,7 @@
    4.31      ctxt'' |>
    4.32      Proof.theorem_i NONE (fn thss => fn ctxt =>
    4.33        let
    4.34 -        val rec_name = space_implode "_" (map NameSpace.base_name names);
    4.35 +        val rec_name = space_implode "_" (map Long_Name.base_name names);
    4.36          val rec_qualified = Binding.qualify false rec_name;
    4.37          val ind_case_names = RuleCases.case_names induct_cases;
    4.38          val induct_cases' = InductivePackage.partition_rules' raw_induct
     5.1 --- a/src/HOL/Nominal/nominal_package.ML	Sun Mar 08 17:19:15 2009 +0100
     5.2 +++ b/src/HOL/Nominal/nominal_package.ML	Sun Mar 08 17:26:14 2009 +0100
     5.3 @@ -49,9 +49,9 @@
     5.4  
     5.5  fun dt_cases (descr: descr) (_, args, constrs) =
     5.6    let
     5.7 -    fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     5.8 +    fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     5.9      val bnames = map the_bname (distinct op = (List.concat (map dt_recs args)));
    5.10 -  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
    5.11 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    5.12  
    5.13  
    5.14  fun induct_cases descr =
    5.15 @@ -364,7 +364,7 @@
    5.16          val pi2 = Free ("pi2", permT);
    5.17          val pt_inst = pt_inst_of thy2 a;
    5.18          val pt2' = pt_inst RS pt2;
    5.19 -        val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    5.20 +        val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a);
    5.21        in List.take (map standard (split_conj_thm
    5.22          (Goal.prove_global thy2 [] []
    5.23             (augment_sort thy2 [pt_class_of thy2 a]
    5.24 @@ -399,7 +399,7 @@
    5.25          val pt_inst = pt_inst_of thy2 a;
    5.26          val pt3' = pt_inst RS pt3;
    5.27          val pt3_rev' = at_inst RS (pt_inst RS pt3_rev);
    5.28 -        val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    5.29 +        val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a);
    5.30        in List.take (map standard (split_conj_thm
    5.31          (Goal.prove_global thy2 [] []
    5.32            (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies
    5.33 @@ -665,7 +665,7 @@
    5.34                asm_full_simp_tac (simpset_of thy addsimps
    5.35                  [Rep RS perm_closed RS Abs_inverse]) 1,
    5.36                asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
    5.37 -                ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy
    5.38 +                ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
    5.39            end)
    5.40          (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~
    5.41             new_type_names ~~ tyvars ~~ perm_closed_thms);
    5.42 @@ -729,8 +729,8 @@
    5.43  
    5.44      (** strips the "_Rep" in type names *)
    5.45      fun strip_nth_name i s =
    5.46 -      let val xs = NameSpace.explode s;
    5.47 -      in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    5.48 +      let val xs = Long_Name.explode s;
    5.49 +      in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end;
    5.50  
    5.51      val (descr'', ndescr) = ListPair.unzip (List.mapPartial
    5.52        (fn (i, ("Nominal.noption", _, _)) => NONE
    5.53 @@ -799,7 +799,7 @@
    5.54          val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs);
    5.55          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    5.56            (Const (rep_name, T --> T') $ lhs, rhs));
    5.57 -        val def_name = (NameSpace.base_name cname) ^ "_def";
    5.58 +        val def_name = (Long_Name.base_name cname) ^ "_def";
    5.59          val ([def_thm], thy') = thy |>
    5.60            Sign.add_consts_i [(Binding.name cname', constrT, mx)] |>
    5.61            (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)]
    5.62 @@ -890,7 +890,7 @@
    5.63            map (fn ((cname, dts), constr_rep_thm) =>
    5.64          let
    5.65            val cname = Sign.intern_const thy8
    5.66 -            (NameSpace.append tname (NameSpace.base_name cname));
    5.67 +            (Long_Name.append tname (Long_Name.base_name cname));
    5.68            val permT = mk_permT (Type (atom, []));
    5.69            val pi = Free ("pi", permT);
    5.70  
    5.71 @@ -946,7 +946,7 @@
    5.72          if null dts then NONE else SOME
    5.73          let
    5.74            val cname = Sign.intern_const thy8
    5.75 -            (NameSpace.append tname (NameSpace.base_name cname));
    5.76 +            (Long_Name.append tname (Long_Name.base_name cname));
    5.77  
    5.78            fun make_inj ((dts, dt), (j, args1, args2, eqs)) =
    5.79              let
    5.80 @@ -988,7 +988,7 @@
    5.81        in List.concat (map (fn (cname, dts) => map (fn atom =>
    5.82          let
    5.83            val cname = Sign.intern_const thy8
    5.84 -            (NameSpace.append tname (NameSpace.base_name cname));
    5.85 +            (Long_Name.append tname (Long_Name.base_name cname));
    5.86            val atomT = Type (atom, []);
    5.87  
    5.88            fun process_constr ((dts, dt), (j, args1, args2)) =
    5.89 @@ -1101,7 +1101,7 @@
    5.90             (fn _ => indtac dt_induct indnames 1 THEN
    5.91              ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
    5.92                (abs_supp @ supp_atm @
    5.93 -               PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @
    5.94 +               PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
    5.95                 List.concat supp_thms))))),
    5.96           length new_type_names))
    5.97        end) atoms;
    5.98 @@ -1233,9 +1233,9 @@
    5.99      val fin_set_fresh = map (fn s =>
   5.100        at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms;
   5.101      val pt1_atoms = map (fn Type (s, _) =>
   5.102 -      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs;
   5.103 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs;
   5.104      val pt2_atoms = map (fn Type (s, _) =>
   5.105 -      PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs;
   5.106 +      PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs;
   5.107      val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'";
   5.108      val fs_atoms = PureThy.get_thms thy9 "fin_supp";
   5.109      val abs_supp = PureThy.get_thms thy9 "abs_supp";
   5.110 @@ -1514,7 +1514,7 @@
   5.111            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
   5.112            (map dest_Free rec_fns)
   5.113            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
   5.114 -      PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct");
   5.115 +      PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
   5.116  
   5.117      (** equivariance **)
   5.118  
   5.119 @@ -1560,7 +1560,7 @@
   5.120  
   5.121      val rec_fin_supp_thms = map (fn aT =>
   5.122        let
   5.123 -        val name = NameSpace.base_name (fst (dest_Type aT));
   5.124 +        val name = Long_Name.base_name (fst (dest_Type aT));
   5.125          val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   5.126          val aset = HOLogic.mk_setT aT;
   5.127          val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT);
   5.128 @@ -1599,7 +1599,7 @@
   5.129  
   5.130      val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) =>
   5.131        let
   5.132 -        val name = NameSpace.base_name (fst (dest_Type aT));
   5.133 +        val name = Long_Name.base_name (fst (dest_Type aT));
   5.134          val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1");
   5.135          val a = Free ("a", aT);
   5.136          val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop
   5.137 @@ -2013,10 +2013,10 @@
   5.138      val (reccomb_defs, thy12) =
   5.139        thy11
   5.140        |> Sign.add_consts_i (map (fn ((name, T), T') =>
   5.141 -          (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
   5.142 +          (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn))
   5.143            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   5.144        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   5.145 -          (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   5.146 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   5.147             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   5.148               set $ Free ("x", T) $ Free ("y", T'))))))
   5.149                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts));
     6.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Sun Mar 08 17:19:15 2009 +0100
     6.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Sun Mar 08 17:26:14 2009 +0100
     6.3 @@ -110,7 +110,7 @@
     6.4            Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
     6.5              (if (applicable_app f) then
     6.6                let
     6.7 -                val name = NameSpace.base_name n
     6.8 +                val name = Long_Name.base_name n
     6.9                  val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst")
    6.10                  val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst")
    6.11                in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end
    6.12 @@ -198,8 +198,8 @@
    6.13           Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
    6.14            pi2 $ t)) =>
    6.15      let
    6.16 -      val tname' = NameSpace.base_name tname
    6.17 -      val uname' = NameSpace.base_name uname
    6.18 +      val tname' = Long_Name.base_name tname
    6.19 +      val uname' = Long_Name.base_name uname
    6.20      in
    6.21        if pi1 <> pi2 then  (* only apply the composition rule in this case *)
    6.22          if T = U then    
     7.1 --- a/src/HOL/Nominal/nominal_primrec.ML	Sun Mar 08 17:19:15 2009 +0100
     7.2 +++ b/src/HOL/Nominal/nominal_primrec.ML	Sun Mar 08 17:26:14 2009 +0100
     7.3 @@ -207,7 +207,7 @@
     7.4      val frees = ls @ x :: rs;
     7.5      val raw_rhs = list_abs_free (frees,
     7.6        list_comb (Const (rec_name, dummyT), fs @ [Free x]))
     7.7 -    val def_name = Thm.def_name (NameSpace.base_name fname);
     7.8 +    val def_name = Thm.def_name (Long_Name.base_name fname);
     7.9      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
    7.10      val SOME var = get_first (fn ((b, _), mx) =>
    7.11        if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
    7.12 @@ -286,7 +286,7 @@
    7.13        fold_map (apfst (snd o snd) oo
    7.14          LocalTheory.define Thm.definitionK o fst) defs';
    7.15      val qualify = Binding.qualify false
    7.16 -      (space_implode "_" (map (NameSpace.base_name o #1) defs));
    7.17 +      (space_implode "_" (map (Long_Name.base_name o #1) defs));
    7.18      val names_atts' = map (apfst qualify) names_atts;
    7.19      val cert = cterm_of (ProofContext.theory_of lthy');
    7.20  
     8.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 08 17:19:15 2009 +0100
     8.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Mar 08 17:26:14 2009 +0100
     8.3 @@ -115,7 +115,7 @@
     8.4                 (Var (n,ty))) =>
     8.5               let
     8.6                  (* FIXME: this should be an operation the library *)
     8.7 -                val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm)
     8.8 +                val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm)
     8.9               in
    8.10                  if (Sign.of_sort thy (ty,[class_name]))
    8.11                  then [(pi,typi)]
     9.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Mar 08 17:19:15 2009 +0100
     9.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Mar 08 17:26:14 2009 +0100
     9.3 @@ -336,17 +336,17 @@
     9.4      [] => ""
     9.5     | c::cs => String.implode (Char.toUpper c::cs ))
     9.6  
     9.7 -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T)
     9.8 -  | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x)
     9.9 -  | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x);
    9.10 +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T)
    9.11 +  | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x)
    9.12 +  | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x);
    9.13  
    9.14  fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n);
    9.15  
    9.16  fun mk_map "List.list" = Syntax.const "List.map"
    9.17 -  | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n);
    9.18 +  | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n);
    9.19  
    9.20  fun gen_constr_destr comp prfx thy (Type (T,[])) = 
    9.21 -      Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))
    9.22 +      Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))
    9.23    | gen_constr_destr comp prfx thy (T as Type ("fun",_)) =
    9.24       let val (argTs,rangeT) = strip_type T;
    9.25       in comp 
    9.26 @@ -360,11 +360,11 @@
    9.27       then (* datatype args are recursively embedded into val *)
    9.28           (case argTs of
    9.29             [argT] => comp 
    9.30 -                     ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T)))))
    9.31 +                     ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T)))))
    9.32                       ((mk_map T $ gen_constr_destr comp prfx thy argT))
    9.33            | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[])))
    9.34       else (* type args are not recursively embedded into val *)
    9.35 -           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T)))
    9.36 +           Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T)))
    9.37    | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[]));
    9.38                     
    9.39  val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) ""
    10.1 --- a/src/HOL/Statespace/state_space.ML	Sun Mar 08 17:19:15 2009 +0100
    10.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Mar 08 17:26:14 2009 +0100
    10.3 @@ -645,7 +645,7 @@
    10.4  fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s;
    10.5  
    10.6  fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] =
    10.7 -     if NameSpace.base_name k = NameSpace.base_name KN then
    10.8 +     if Long_Name.base_name k = Long_Name.base_name KN then
    10.9          (case get_comp (Context.Proof ctxt) name of
   10.10            SOME (T,_) => if inj=inject_name T andalso prj=project_name T then
   10.11                             Syntax.const "_statespace_update" $ s $ n $ v
    11.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Mar 08 17:19:15 2009 +0100
    11.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 08 17:26:14 2009 +0100
    11.3 @@ -223,7 +223,7 @@
    11.4   *---------------------------------------------------------------------------*)
    11.5  fun define_i strict thy cs ss congs wfs fid R eqs =
    11.6    let val {functional,pats} = Prim.mk_functional thy eqs
    11.7 -      val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional
    11.8 +      val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional
    11.9        val {induct, rules, tcs} = 
   11.10            simplify_defn strict thy cs ss congs wfs fid pats def
   11.11        val rules' = 
   11.12 @@ -248,7 +248,7 @@
   11.13  
   11.14  fun defer_i thy congs fid eqs =
   11.15   let val {rules,R,theory,full_pats_TCs,SV,...} =
   11.16 -             Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs
   11.17 +             Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs
   11.18       val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules));
   11.19       val dummy = writeln "Proving induction theorem ...";
   11.20       val induction = Prim.mk_induction theory
    12.1 --- a/src/HOL/Tools/TFL/tfl.ML	Sun Mar 08 17:19:15 2009 +0100
    12.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Sun Mar 08 17:26:14 2009 +0100
    12.3 @@ -349,7 +349,7 @@
    12.4            | L => mk_functional_err
    12.5   ("The following clauses are redundant (covered by preceding clauses): " ^
    12.6                     commas (map (fn i => Int.toString (i + 1)) L))
    12.7 - in {functional = Abs(NameSpace.base_name fname, ftype,
    12.8 + in {functional = Abs(Long_Name.base_name fname, ftype,
    12.9                        abstract_over (atom,
   12.10                                       absfree(aname,atype, case_tm))),
   12.11       pats = patts2}
    13.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sun Mar 08 17:19:15 2009 +0100
    13.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sun Mar 08 17:26:14 2009 +0100
    13.3 @@ -235,10 +235,10 @@
    13.4      val (reccomb_defs, thy2) =
    13.5        thy1
    13.6        |> Sign.add_consts_i (map (fn ((name, T), T') =>
    13.7 -          (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
    13.8 +          (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn))
    13.9            (reccomb_names ~~ recTs ~~ rec_result_Ts))
   13.10        |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') =>
   13.11 -          (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   13.12 +          (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T,
   13.13             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
   13.14               set $ Free ("x", T) $ Free ("y", T'))))))
   13.15                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
   13.16 @@ -316,8 +316,8 @@
   13.17            val fns = (List.concat (Library.take (i, case_dummy_fns))) @
   13.18              fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns)));
   13.19            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
   13.20 -          val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn);
   13.21 -          val def = (Binding.name (NameSpace.base_name name ^ "_def"),
   13.22 +          val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
   13.23 +          val def = (Binding.name (Long_Name.base_name name ^ "_def"),
   13.24              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
   13.25                list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @
   13.26                  fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) )));
    14.1 --- a/src/HOL/Tools/datatype_aux.ML	Sun Mar 08 17:19:15 2009 +0100
    14.2 +++ b/src/HOL/Tools/datatype_aux.ML	Sun Mar 08 17:26:14 2009 +0100
    14.3 @@ -224,7 +224,7 @@
    14.4    | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
    14.5  
    14.6  fun name_of_typ (Type (s, Ts)) =
    14.7 -      let val s' = NameSpace.base_name s
    14.8 +      let val s' = Long_Name.base_name s
    14.9        in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @
   14.10          [if Syntax.is_identifier s' then s' else "x"])
   14.11        end
    15.1 --- a/src/HOL/Tools/datatype_package.ML	Sun Mar 08 17:19:15 2009 +0100
    15.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun Mar 08 17:26:14 2009 +0100
    15.3 @@ -174,9 +174,9 @@
    15.4  
    15.5  fun dt_cases (descr: descr) (_, args, constrs) =
    15.6    let
    15.7 -    fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i)));
    15.8 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
    15.9      val bnames = map the_bname (distinct (op =) (maps dt_recs args));
   15.10 -  in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end;
   15.11 +  in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
   15.12  
   15.13  
   15.14  fun induct_cases descr =
   15.15 @@ -519,7 +519,7 @@
   15.16      val cs = map (apsnd (map norm_constr)) raw_cs;
   15.17      val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
   15.18        o fst o strip_type;
   15.19 -    val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names);
   15.20 +    val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
   15.21  
   15.22      fun mk_spec (i, (tyco, constr)) = (i, (tyco,
   15.23        map (DtTFree o fst) vs,
    16.1 --- a/src/HOL/Tools/datatype_prop.ML	Sun Mar 08 17:19:15 2009 +0100
    16.2 +++ b/src/HOL/Tools/datatype_prop.ML	Sun Mar 08 17:26:14 2009 +0100
    16.3 @@ -47,7 +47,7 @@
    16.4    let
    16.5      fun type_name (TFree (name, _)) = implode (tl (explode name))
    16.6        | type_name (Type (name, _)) = 
    16.7 -          let val name' = NameSpace.base_name name
    16.8 +          let val name' = Long_Name.base_name name
    16.9            in if Syntax.is_identifier name' then name' else "x" end;
   16.10    in indexify_names (map type_name Ts) end;
   16.11  
    17.1 --- a/src/HOL/Tools/datatype_realizer.ML	Sun Mar 08 17:19:15 2009 +0100
    17.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Sun Mar 08 17:26:14 2009 +0100
    17.3 @@ -168,7 +168,7 @@
    17.4          val Ts = map (typ_of_dtyp descr sorts) cargs;
    17.5          val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts;
    17.6          val free_ts = map Free frees;
    17.7 -        val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT)
    17.8 +        val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
    17.9        in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop
   17.10          (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
   17.11            HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $
    18.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 08 17:19:15 2009 +0100
    18.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Sun Mar 08 17:26:14 2009 +0100
    18.3 @@ -236,7 +236,7 @@
    18.4          val lhs = list_comb (Const (cname, constrT), l_args);
    18.5          val rhs = mk_univ_inj r_args n i;
    18.6          val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs);
    18.7 -        val def_name = NameSpace.base_name cname ^ "_def";
    18.8 +        val def_name = Long_Name.base_name cname ^ "_def";
    18.9          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
   18.10            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
   18.11          val ([def_thm], thy') =
   18.12 @@ -343,7 +343,7 @@
   18.13          
   18.14          val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds);
   18.15          val fTs = map fastype_of fs;
   18.16 -        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"),
   18.17 +        val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"),
   18.18            Logic.mk_equals (Const (iso_name, T --> Univ_elT),
   18.19              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos);
   18.20          val (def_thms, thy') =
    19.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun Mar 08 17:19:15 2009 +0100
    19.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun Mar 08 17:26:14 2009 +0100
    19.3 @@ -54,7 +54,7 @@
    19.4        val simps_by_f = sort saved_simps
    19.5  
    19.6        fun add_for_f fname simps =
    19.7 -        note_theorem ((NameSpace.qualified fname label, []), simps) #> snd
    19.8 +        note_theorem ((Long_Name.qualify fname label, []), simps) #> snd
    19.9      in
   19.10        (saved_simps,
   19.11         fold2 add_for_f fnames simps_by_f lthy)
   19.12 @@ -66,12 +66,12 @@
   19.13            cont (Thm.close_derivation proof)
   19.14  
   19.15        val fnames = map (fst o fst) fixes
   19.16 -      val qualify = NameSpace.qualified defname
   19.17 +      val qualify = Long_Name.qualify defname
   19.18        val addsmps = add_simps fnames post sort_cont
   19.19  
   19.20        val (((psimps', pinducts'), (_, [termination'])), lthy) =
   19.21            lthy
   19.22 -            |> addsmps (NameSpace.qualified "partial") "psimps"
   19.23 +            |> addsmps (Long_Name.qualify "partial") "psimps"
   19.24                         [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps
   19.25              ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps
   19.26              ||>> note_theorem ((qualify "pinduct",
   19.27 @@ -131,7 +131,7 @@
   19.28        val allatts = (not has_guards ? cons Code.add_default_eqn_attrib)
   19.29          [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]
   19.30  
   19.31 -      val qualify = NameSpace.qualified defname;
   19.32 +      val qualify = Long_Name.qualify defname;
   19.33      in
   19.34        lthy
   19.35          |> add_simps I "simps" allatts tsimps |> snd
    20.1 --- a/src/HOL/Tools/function_package/size.ML	Sun Mar 08 17:19:15 2009 +0100
    20.2 +++ b/src/HOL/Tools/function_package/size.ML	Sun Mar 08 17:26:14 2009 +0100
    20.3 @@ -87,7 +87,7 @@
    20.4        recTs1 ~~ alt_names' |>
    20.5        map (fn (T as Type (s, _), optname) =>
    20.6          let
    20.7 -          val s' = the_default (NameSpace.base_name s) optname ^ "_size";
    20.8 +          val s' = the_default (Long_Name.base_name s) optname ^ "_size";
    20.9            val s'' = Sign.full_bname thy s'
   20.10          in
   20.11            (s'',
   20.12 @@ -140,7 +140,7 @@
   20.13      val ((size_def_thms, size_def_thms'), thy') =
   20.14        thy
   20.15        |> Sign.add_consts_i (map (fn (s, T) =>
   20.16 -           (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
   20.17 +           (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn))
   20.18             (size_names ~~ recTs1))
   20.19        |> PureThy.add_defs false
   20.20          (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs)))
   20.21 @@ -221,8 +221,8 @@
   20.22  fun add_size_thms (new_type_names as name :: _) thy =
   20.23    let
   20.24      val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
   20.25 -    val prefix = NameSpace.map_base_name (K (space_implode "_"
   20.26 -      (the_default (map NameSpace.base_name new_type_names) alt_names))) name;
   20.27 +    val prefix = Long_Name.map_base_name (K (space_implode "_"
   20.28 +      (the_default (map Long_Name.base_name new_type_names) alt_names))) name;
   20.29      val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
   20.30        is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
   20.31    in if no_size then thy
    21.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Mar 08 17:19:15 2009 +0100
    21.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Mar 08 17:26:14 2009 +0100
    21.3 @@ -698,7 +698,7 @@
    21.4        ctxt1 |>
    21.5        LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>>
    21.6        fold_map (fn (name, (elim, cases)) =>
    21.7 -        LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"),
    21.8 +        LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"),
    21.9            [Attrib.internal (K (RuleCases.case_names cases)),
   21.10             Attrib.internal (K (RuleCases.consumes 1)),
   21.11             Attrib.internal (K (Induct.cases_pred name)),
    22.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 08 17:19:15 2009 +0100
    22.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 08 17:26:14 2009 +0100
    22.3 @@ -68,8 +68,8 @@
    22.4      val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop
    22.5        (Logic.strip_imp_concl (prop_of (hd intrs))));
    22.6      val params = map dest_Var (Library.take (nparms, ts));
    22.7 -    val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs));
    22.8 -    fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)),
    22.9 +    val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs));
   22.10 +    fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)),
   22.11        map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
   22.12          filter_out (equal Extraction.nullT) (map
   22.13            (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
   22.14 @@ -112,7 +112,7 @@
   22.15      val rT = if n then Extraction.nullT
   22.16        else Type (space_implode "_" (s ^ "T" :: vs),
   22.17          map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs);
   22.18 -    val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT);
   22.19 +    val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT);
   22.20      val S = list_comb (h, params @ xs);
   22.21      val rvs = relevant_vars S;
   22.22      val vs' = map fst rvs \\ vs;
   22.23 @@ -195,7 +195,7 @@
   22.24            in if conclT = Extraction.nullT
   22.25              then list_abs_free (map dest_Free xs, HOLogic.unit)
   22.26              else list_abs_free (map dest_Free xs, list_comb
   22.27 -              (Free ("r" ^ NameSpace.base_name (name_of_thm intr),
   22.28 +              (Free ("r" ^ Long_Name.base_name (name_of_thm intr),
   22.29                  map fastype_of (rev args) ---> conclT), rev args))
   22.30            end
   22.31  
   22.32 @@ -217,7 +217,7 @@
   22.33        end) (premss ~~ dummies);
   22.34      val frees = fold Term.add_frees fs [];
   22.35      val Ts = map fastype_of fs;
   22.36 -    fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr)
   22.37 +    fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr)
   22.38    in
   22.39      fst (fold_map (fn concl => fn names =>
   22.40        let val T = Extraction.etype_of thy vs [] concl
   22.41 @@ -245,7 +245,7 @@
   22.42        |-> (fn dtinfo => pair (map fst dts, SOME dtinfo))
   22.43      handle DatatypeAux.Datatype_Empty name' =>
   22.44        let
   22.45 -        val name = NameSpace.base_name name';
   22.46 +        val name = Long_Name.base_name name';
   22.47          val dname = Name.variant used "Dummy";
   22.48        in
   22.49          thy
   22.50 @@ -273,8 +273,8 @@
   22.51  
   22.52  fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   22.53    let
   22.54 -    val qualifier = NameSpace.qualifier (name_of_thm induct);
   22.55 -    val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts");
   22.56 +    val qualifier = Long_Name.qualifier (name_of_thm induct);
   22.57 +    val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts");
   22.58      val iTs = OldTerm.term_tvars (prop_of (hd intrs));
   22.59      val ar = length vs + length iTs;
   22.60      val params = InductivePackage.params_of raw_induct;
   22.61 @@ -285,18 +285,18 @@
   22.62      val rss' = map (fn (((s, rs), (_, arity)), elim) =>
   22.63        (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs)))
   22.64          (rss ~~ arities ~~ elims);
   22.65 -    val (prfx, _) = split_last (NameSpace.explode (fst (hd rss)));
   22.66 +    val (prfx, _) = split_last (Long_Name.explode (fst (hd rss)));
   22.67      val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets;
   22.68  
   22.69      val thy1 = thy |>
   22.70        Sign.root_path |>
   22.71 -      Sign.add_path (NameSpace.implode prfx);
   22.72 +      Sign.add_path (Long_Name.implode prfx);
   22.73      val (ty_eqs, rlz_eqs) = split_list
   22.74        (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
   22.75  
   22.76      val thy1' = thy1 |>
   22.77        Theory.copy |>
   22.78 -      Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |>
   22.79 +      Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
   22.80        fold (fn s => AxClass.axiomatize_arity
   22.81          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
   22.82          Extraction.add_typeof_eqns_i ty_eqs;
   22.83 @@ -334,7 +334,7 @@
   22.84        rintrs |> map (fn rintr =>
   22.85          let
   22.86            val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr));
   22.87 -          val s' = NameSpace.base_name s;
   22.88 +          val s' = Long_Name.base_name s;
   22.89            val T' = Logic.unvarifyT T;
   22.90          in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end)
   22.91        |> distinct (op = o pairself (#1 o #1))
   22.92 @@ -352,7 +352,7 @@
   22.93          {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
   22.94            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
   22.95          rlzpreds rlzparams (map (fn (rintr, intr) =>
   22.96 -          ((Binding.name (NameSpace.base_name (name_of_thm intr)), []),
   22.97 +          ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
   22.98             subst_atomic rlzpreds' (Logic.unvarify rintr)))
   22.99               (rintrs ~~ maps snd rss)) [] ||>
  22.100        Sign.absolute_path;
  22.101 @@ -395,12 +395,12 @@
  22.102               [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
  22.103                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
  22.104          val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_"
  22.105 -          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
  22.106 +          (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
  22.107          val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
  22.108            (DatatypeAux.split_conj_thm thm');
  22.109          val ([thms'], thy'') = PureThy.add_thmss
  22.110            [((Binding.name (space_implode "_"
  22.111 -             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
  22.112 +             (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @
  22.113                 ["correctness"])), thms), [])] thy';
  22.114          val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
  22.115        in
  22.116 @@ -409,7 +409,7 @@
  22.117                mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
  22.118              realizers @ (case realizers of
  22.119               [(((ind, corr), rlz), r)] =>
  22.120 -               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
  22.121 +               [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct",
  22.122                    ind, corr, rlz, r)]
  22.123             | _ => [])) thy''
  22.124        end;
    23.1 --- a/src/HOL/Tools/old_primrec_package.ML	Sun Mar 08 17:19:15 2009 +0100
    23.2 +++ b/src/HOL/Tools/old_primrec_package.ML	Sun Mar 08 17:26:14 2009 +0100
    23.3 @@ -212,7 +212,7 @@
    23.4                      ((map snd ls) @ [dummyT])
    23.5                      (list_comb (Const (rec_name, dummyT),
    23.6                                  fs @ map Bound (0 ::(length ls downto 1))))
    23.7 -    val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def";
    23.8 +    val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def";
    23.9      val def_prop =
   23.10        singleton (Syntax.check_terms (ProofContext.init thy))
   23.11          (Logic.mk_equals (Const (fname, dummyT), rhs));
   23.12 @@ -269,7 +269,7 @@
   23.13              else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
   23.14                "\nare not mutually recursive");
   23.15      val primrec_name =
   23.16 -      if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name;
   23.17 +      if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name;
   23.18      val (defs_thms', thy') =
   23.19        thy
   23.20        |> Sign.add_path primrec_name
    24.1 --- a/src/HOL/Tools/primrec_package.ML	Sun Mar 08 17:19:15 2009 +0100
    24.2 +++ b/src/HOL/Tools/primrec_package.ML	Sun Mar 08 17:26:14 2009 +0100
    24.3 @@ -191,7 +191,7 @@
    24.4                      (map snd ls @ [dummyT])
    24.5                      (list_comb (Const (rec_name, dummyT),
    24.6                                  fs @ map Bound (0 :: (length ls downto 1))))
    24.7 -    val def_name = Thm.def_name (NameSpace.base_name fname);
    24.8 +    val def_name = Thm.def_name (Long_Name.base_name fname);
    24.9      val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
   24.10      val SOME var = get_first (fn ((b, _), mx) =>
   24.11        if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes;
   24.12 @@ -247,7 +247,7 @@
   24.13      val _ = if gen_eq_set (op =) (names1, names2) then ()
   24.14        else primrec_error ("functions " ^ commas_quote names2 ^
   24.15          "\nare not mutually recursive");
   24.16 -    val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs);
   24.17 +    val prefix = space_implode "_" (map (Long_Name.base_name o #1) defs);
   24.18      val qualify = Binding.qualify false prefix;
   24.19      val spec' = (map o apfst)
   24.20        (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec;
    25.1 --- a/src/HOL/Tools/recdef_package.ML	Sun Mar 08 17:19:15 2009 +0100
    25.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun Mar 08 17:26:14 2009 +0100
    25.3 @@ -193,7 +193,7 @@
    25.4      val _ = requires_recdef thy;
    25.5  
    25.6      val name = Sign.intern_const thy raw_name;
    25.7 -    val bname = NameSpace.base_name name;
    25.8 +    val bname = Long_Name.base_name name;
    25.9      val _ = writeln ("Defining recursive function " ^ quote name ^ " ...");
   25.10  
   25.11      val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs);
   25.12 @@ -233,7 +233,7 @@
   25.13  fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy =
   25.14    let
   25.15      val name = Sign.intern_const thy raw_name;
   25.16 -    val bname = NameSpace.base_name name;
   25.17 +    val bname = Long_Name.base_name name;
   25.18  
   25.19      val _ = requires_recdef thy;
   25.20      val _ = writeln ("Deferred recursive function " ^ quote name ^ " ...");
    26.1 --- a/src/HOL/Tools/record_package.ML	Sun Mar 08 17:19:15 2009 +0100
    26.2 +++ b/src/HOL/Tools/record_package.ML	Sun Mar 08 17:26:14 2009 +0100
    26.3 @@ -122,7 +122,7 @@
    26.4  (* syntax *)
    26.5  
    26.6  fun prune n xs = Library.drop (n, xs);
    26.7 -fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname);
    26.8 +fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname);
    26.9  
   26.10  val Trueprop = HOLogic.mk_Trueprop;
   26.11  fun All xs t = Term.list_all_free (xs, t);
   26.12 @@ -433,8 +433,8 @@
   26.13  fun get_extT_fields thy T =
   26.14    let
   26.15      val ((name,Ts),moreT) = dest_recT T;
   26.16 -    val recname = let val (nm::recn::rst) = rev (NameSpace.explode name)
   26.17 -                  in NameSpace.implode (rev (nm::rst)) end;
   26.18 +    val recname = let val (nm::recn::rst) = rev (Long_Name.explode name)
   26.19 +                  in Long_Name.implode (rev (nm::rst)) end;
   26.20      val midx = maxidx_of_typs (moreT::Ts);
   26.21      val varifyT = varifyT midx;
   26.22      val {records,extfields,...} = RecordsData.get thy;
   26.23 @@ -702,7 +702,7 @@
   26.24                       SOME flds
   26.25                       => (let
   26.26                            val (f::fs) = but_last (map fst flds);
   26.27 -                          val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs;
   26.28 +                          val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs;
   26.29                            val (args',more) = split_last args;
   26.30                           in (flds'~~args')@field_lst more end
   26.31                           handle Library.UnequalLengths => [("",t)])
   26.32 @@ -804,7 +804,7 @@
   26.33                             => (let
   26.34                                  val (f :: fs) = but_last flds;
   26.35                                  val flds' = apfst (Sign.extern_const thy) f
   26.36 -                                  :: map (apfst NameSpace.base_name) fs;
   26.37 +                                  :: map (apfst Long_Name.base_name) fs;
   26.38                                  val (args', more) = split_last args;
   26.39                                  val alphavars = map varifyT (but_last alphas);
   26.40                                  val subst = fold2 (curry (Sign.typ_match thy))
   26.41 @@ -1069,7 +1069,7 @@
   26.42               val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy;
   26.43  
   26.44               (*fun mk_abs_var x t = (x, fastype_of t);*)
   26.45 -             fun sel_name u = NameSpace.base_name (unsuffix updateN u);
   26.46 +             fun sel_name u = Long_Name.base_name (unsuffix updateN u);
   26.47  
   26.48               fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) =
   26.49                    if has_field extfields s (domain_type' mT) then upd else seed s r
   26.50 @@ -1461,7 +1461,7 @@
   26.51            Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name;
   26.52          val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp];
   26.53        in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end;
   26.54 -    val tname = Binding.name (NameSpace.base_name name);
   26.55 +    val tname = Binding.name (Long_Name.base_name name);
   26.56    in
   26.57      thy
   26.58      |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE
   26.59 @@ -1475,7 +1475,7 @@
   26.60  
   26.61  fun extension_definition full name fields names alphas zeta moreT more vars thy =
   26.62    let
   26.63 -    val base = NameSpace.base_name;
   26.64 +    val base = Long_Name.base_name;
   26.65      val fieldTs = (map snd fields);
   26.66      val alphas_zeta = alphas@[zeta];
   26.67      val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta;
   26.68 @@ -1761,7 +1761,7 @@
   26.69      val alphas = map fst args;
   26.70      val name = Sign.full_bname thy bname;
   26.71      val full = Sign.full_bname_path thy bname;
   26.72 -    val base = NameSpace.base_name;
   26.73 +    val base = Long_Name.base_name;
   26.74  
   26.75      val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields);
   26.76  
   26.77 @@ -1887,11 +1887,11 @@
   26.78  
   26.79      fun parent_more s =
   26.80           if null parents then s
   26.81 -         else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT);
   26.82 +         else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT);
   26.83  
   26.84      fun parent_more_upd v s =
   26.85        if null parents then v$s
   26.86 -      else let val mp = NameSpace.qualified (#name (List.last parents)) moreN;
   26.87 +      else let val mp = Long_Name.qualify (#name (List.last parents)) moreN;
   26.88             in mk_upd updateN mp v s end;
   26.89  
   26.90      (*record (scheme) type abbreviation*)
    27.1 --- a/src/HOL/Tools/res_atp.ML	Sun Mar 08 17:19:15 2009 +0100
    27.2 +++ b/src/HOL/Tools/res_atp.ML	Sun Mar 08 17:26:14 2009 +0100
    27.3 @@ -303,7 +303,7 @@
    27.4  (*Reject theorems with names like "List.filter.filter_list_def" or
    27.5    "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
    27.6  fun is_package_def a =
    27.7 -  let val names = NameSpace.explode a
    27.8 +  let val names = Long_Name.explode a
    27.9    in
   27.10       length names > 2 andalso
   27.11       not (hd names = "local") andalso
   27.12 @@ -378,7 +378,7 @@
   27.13  
   27.14  (*Ignore blacklisted basenames*)
   27.15  fun add_multi_names ((a, ths), pairs) =
   27.16 -  if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   27.17 +  if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   27.18    else add_single_names ((a, ths), pairs);
   27.19  
   27.20  fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
    28.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:19:15 2009 +0100
    28.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 08 17:26:14 2009 +0100
    28.3 @@ -328,7 +328,7 @@
    28.4     "cases","ext_cases"];  (*FIXME: put other record thms here, or use the "Internal" marker*)
    28.5  
    28.6  (*Keep the full complexity of the original name*)
    28.7 -fun flatten_name s = space_implode "_X" (NameSpace.explode s);
    28.8 +fun flatten_name s = space_implode "_X" (Long_Name.explode s);
    28.9  
   28.10  fun fake_name th =
   28.11    if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
   28.12 @@ -340,7 +340,7 @@
   28.13  
   28.14  (*Skolemize a named theorem, with Skolem functions as additional premises.*)
   28.15  fun skolem_thm (s, th) =
   28.16 -  if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then []
   28.17 +  if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then []
   28.18    else
   28.19      let
   28.20        val ctxt0 = Variable.thm_context th
   28.21 @@ -428,7 +428,7 @@
   28.22      val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) =>
   28.23        if already_seen thy name then I else cons (name, ths));
   28.24      val new_thms = (new_facts, []) |-> fold (fn (name, ths) =>
   28.25 -      if member (op =) multi_base_blacklist (NameSpace.base_name name) then I
   28.26 +      if member (op =) multi_base_blacklist (Long_Name.base_name name) then I
   28.27        else fold_index (fn (i, th) =>
   28.28          if bad_for_atp th orelse is_some (lookup_cache thy th) then I
   28.29          else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths);
    29.1 --- a/src/HOL/Tools/specification_package.ML	Sun Mar 08 17:19:15 2009 +0100
    29.2 +++ b/src/HOL/Tools/specification_package.ML	Sun Mar 08 17:26:14 2009 +0100
    29.3 @@ -24,7 +24,7 @@
    29.4                  val ctype = domain_type (type_of P)
    29.5                  val cname_full = Sign.intern_const thy cname
    29.6                  val cdefname = if thname = ""
    29.7 -                               then Thm.def_name (NameSpace.base_name cname)
    29.8 +                               then Thm.def_name (Long_Name.base_name cname)
    29.9                                 else thname
   29.10                  val def_eq = Logic.mk_equals (Const(cname_full,ctype),
   29.11                                                HOLogic.choice_const ctype $  P)
   29.12 @@ -50,7 +50,7 @@
   29.13                          val ctype = domain_type (type_of P)
   29.14                          val cname_full = Sign.intern_const thy cname
   29.15                          val cdefname = if thname = ""
   29.16 -                                       then Thm.def_name (NameSpace.base_name cname)
   29.17 +                                       then Thm.def_name (Long_Name.base_name cname)
   29.18                                         else thname
   29.19                          val co = Const(cname_full,ctype)
   29.20                          val thy' = Theory.add_finals_i covld [co] thy
   29.21 @@ -154,7 +154,7 @@
   29.22          fun mk_exist (c,prop) =
   29.23              let
   29.24                  val T = type_of c
   29.25 -                val cname = NameSpace.base_name (fst (dest_Const c))
   29.26 +                val cname = Long_Name.base_name (fst (dest_Const c))
   29.27                  val vname = if Syntax.is_identifier cname
   29.28                              then cname
   29.29                              else "x"
    30.1 --- a/src/HOL/ex/Quickcheck_Generators.thy	Sun Mar 08 17:19:15 2009 +0100
    30.2 +++ b/src/HOL/ex/Quickcheck_Generators.thy	Sun Mar 08 17:26:14 2009 +0100
    30.3 @@ -138,7 +138,7 @@
    30.4      let
    30.5        val this_ty = Type (hd tycos, map TFree vs);
    30.6        val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed};
    30.7 -      val random_name = NameSpace.base_name @{const_name random};
    30.8 +      val random_name = Long_Name.base_name @{const_name random};
    30.9        val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'";
   30.10        fun random ty = Sign.mk_const thy (@{const_name random}, [ty]);
   30.11        val random' = Free (random'_name,
    31.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Mar 08 17:19:15 2009 +0100
    31.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Sun Mar 08 17:26:14 2009 +0100
    31.3 @@ -22,7 +22,7 @@
    31.4    val dc_rep = %%:(dname^"_rep");
    31.5    val x_name'= "x";
    31.6    val x_name = idx_name eqs x_name' (n+1);
    31.7 -  val dnam = NameSpace.base_name dname;
    31.8 +  val dnam = Long_Name.base_name dname;
    31.9  
   31.10    val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name'));
   31.11    val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
    32.1 --- a/src/HOLCF/Tools/domain/domain_extender.ML	Sun Mar 08 17:19:15 2009 +0100
    32.2 +++ b/src/HOLCF/Tools/domain/domain_extender.ML	Sun Mar 08 17:26:14 2009 +0100
    32.3 @@ -103,7 +103,7 @@
    32.4  			 (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs))
    32.5                     o fst) eqs''';
    32.6      val cons''' = map snd eqs''';
    32.7 -    fun thy_type  (dname,tvars)  = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn);
    32.8 +    fun thy_type  (dname,tvars)  = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn);
    32.9      fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
   32.10      val thy'' = thy''' |> Sign.add_types     (map thy_type  dtnvs)
   32.11  		       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
   32.12 @@ -114,7 +114,7 @@
   32.13      val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
   32.14      fun strip ss = Library.drop (find_index_eq "'" ss +1, ss);
   32.15      fun typid (Type  (id,_)) =
   32.16 -          let val c = hd (Symbol.explode (NameSpace.base_name id))
   32.17 +          let val c = hd (Symbol.explode (Long_Name.base_name id))
   32.18            in if Symbol.is_letter c then c else "t" end
   32.19        | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
   32.20        | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
   32.21 @@ -133,7 +133,7 @@
   32.22        ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
   32.23    in
   32.24      theorems_thy
   32.25 -    |> Sign.add_path (NameSpace.base_name comp_dnam)
   32.26 +    |> Sign.add_path (Long_Name.base_name comp_dnam)
   32.27      |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])]))
   32.28      |> Sign.parent_path
   32.29    end;
    33.1 --- a/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 08 17:19:15 2009 +0100
    33.2 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML	Sun Mar 08 17:26:14 2009 +0100
    33.3 @@ -25,7 +25,7 @@
    33.4  in
    33.5    val dtype  = Type(dname,typevars);
    33.6    val dtype2 = foldr1 mk_ssumT (map prod cons');
    33.7 -  val dnam = NameSpace.base_name dname;
    33.8 +  val dnam = Long_Name.base_name dname;
    33.9    val const_rep  = (dnam^"_rep" ,              dtype  ->> dtype2, NoSyn);
   33.10    val const_abs  = (dnam^"_abs" ,              dtype2 ->> dtype , NoSyn);
   33.11    val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn);
    34.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Mar 08 17:19:15 2009 +0100
    34.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Sun Mar 08 17:26:14 2009 +0100
    34.3 @@ -606,7 +606,7 @@
    34.4  
    34.5  in
    34.6    thy
    34.7 -    |> Sign.add_path (NameSpace.base_name dname)
    34.8 +    |> Sign.add_path (Long_Name.base_name dname)
    34.9      |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [
   34.10          ("iso_rews" , iso_rews  ),
   34.11          ("exhaust"  , [exhaust] ),
    35.1 --- a/src/HOLCF/Tools/fixrec_package.ML	Sun Mar 08 17:19:15 2009 +0100
    35.2 +++ b/src/HOLCF/Tools/fixrec_package.ML	Sun Mar 08 17:26:14 2009 +0100
    35.3 @@ -181,7 +181,7 @@
    35.4      val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss));
    35.5      
    35.6      fun one_def (l as Free(n,_)) r =
    35.7 -          let val b = NameSpace.base_name n
    35.8 +          let val b = Long_Name.base_name n
    35.9            in ((Binding.name (b^"_def"), []), r) end
   35.10        | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form";
   35.11      fun defs [] _ = []
   35.12 @@ -230,7 +230,7 @@
   35.13  
   35.14  fun taken_names (t : term) : bstring list =
   35.15    let
   35.16 -    fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
   35.17 +    fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
   35.18        | taken (Free(a,_) , bs) = insert (op =) a bs
   35.19        | taken (f $ u     , bs) = taken (f, taken (u, bs))
   35.20        | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs)
    36.1 --- a/src/Pure/Isar/class_target.ML	Sun Mar 08 17:19:15 2009 +0100
    36.2 +++ b/src/Pure/Isar/class_target.ML	Sun Mar 08 17:26:14 2009 +0100
    36.3 @@ -300,7 +300,7 @@
    36.4    map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy;
    36.5  
    36.6  fun redeclare_const thy c =
    36.7 -  let val b = NameSpace.base_name c
    36.8 +  let val b = Long_Name.base_name c
    36.9    in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end;
   36.10  
   36.11  fun synchronize_class_syntax sort base_sort ctxt =
   36.12 @@ -358,7 +358,7 @@
   36.13  
   36.14  (* class target *)
   36.15  
   36.16 -val class_prefix = Logic.const_of_class o NameSpace.base_name;
   36.17 +val class_prefix = Logic.const_of_class o Long_Name.base_name;
   36.18  
   36.19  fun declare class pos ((c, mx), dict) thy =
   36.20    let
   36.21 @@ -475,7 +475,7 @@
   36.22  
   36.23  fun type_name "*" = "prod"
   36.24    | type_name "+" = "sum"
   36.25 -  | type_name s = sanatize_name (NameSpace.base_name s);
   36.26 +  | type_name s = sanatize_name (Long_Name.base_name s);
   36.27  
   36.28  fun resort_terms pp algebra consts constraints ts =
   36.29    let
    37.1 --- a/src/Pure/Isar/element.ML	Sun Mar 08 17:19:15 2009 +0100
    37.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 08 17:26:14 2009 +0100
    37.3 @@ -202,7 +202,7 @@
    37.4    let val head =
    37.5      if Thm.has_name_hint th then
    37.6        Pretty.block [Pretty.command kind,
    37.7 -        Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")]
    37.8 +        Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
    37.9      else Pretty.command kind
   37.10    in Pretty.block (Pretty.fbreaks (head :: prts)) end;
   37.11  
   37.12 @@ -522,7 +522,7 @@
   37.13    in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
   37.14  
   37.15  fun check_name name =
   37.16 -  if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   37.17 +  if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   37.18    else name;
   37.19  
   37.20  fun prep_facts prep_name get intern ctxt =
    38.1 --- a/src/Pure/Isar/proof_context.ML	Sun Mar 08 17:19:15 2009 +0100
    38.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Mar 08 17:26:14 2009 +0100
    38.3 @@ -590,7 +590,7 @@
    38.4    let
    38.5      val _ = no_skolem false x;
    38.6      val sko = lookup_skolem ctxt x;
    38.7 -    val is_const = can (read_const_proper ctxt) x orelse NameSpace.is_qualified x;
    38.8 +    val is_const = can (read_const_proper ctxt) x orelse Long_Name.is_qualified x;
    38.9      val is_declared = is_some (def_type (x, ~1));
   38.10    in
   38.11      if Variable.is_const ctxt x then NONE
    39.1 --- a/src/Pure/Isar/proof_display.ML	Sun Mar 08 17:19:15 2009 +0100
    39.2 +++ b/src/Pure/Isar/proof_display.ML	Sun Mar 08 17:26:14 2009 +0100
    39.3 @@ -75,7 +75,7 @@
    39.4  
    39.5  fun pretty_fact_name (kind, "") = Pretty.str kind
    39.6    | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1,
    39.7 -      Pretty.str (NameSpace.base_name name), Pretty.str ":"];
    39.8 +      Pretty.str (Long_Name.base_name name), Pretty.str ":"];
    39.9  
   39.10  fun pretty_facts ctxt =
   39.11    flat o (separate [Pretty.fbrk, Pretty.str "and "]) o
    40.1 --- a/src/Pure/Isar/rule_cases.ML	Sun Mar 08 17:19:15 2009 +0100
    40.2 +++ b/src/Pure/Isar/rule_cases.ML	Sun Mar 08 17:26:14 2009 +0100
    40.3 @@ -105,7 +105,7 @@
    40.4            if not nested then abs_fixes t
    40.5            else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t));
    40.6  
    40.7 -        val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop
    40.8 +        val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
    40.9            |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
   40.10  
   40.11          val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
    41.1 --- a/src/Pure/Isar/theory_target.ML	Sun Mar 08 17:19:15 2009 +0100
    41.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Mar 08 17:26:14 2009 +0100
    41.3 @@ -329,7 +329,7 @@
    41.4  
    41.5  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
    41.6    Data.put ta #>
    41.7 -  LocalTheory.init (NameSpace.base_name target)
    41.8 +  LocalTheory.init (Long_Name.base_name target)
    41.9     {pretty = pretty ta,
   41.10      abbrev = abbrev ta,
   41.11      define = define ta,
    42.1 --- a/src/Pure/ML/ml_antiquote.ML	Sun Mar 08 17:19:15 2009 +0100
    42.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Mar 08 17:26:14 2009 +0100
    42.3 @@ -110,7 +110,7 @@
    42.4  
    42.5  fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) =>
    42.6      #1 (Term.dest_Type (ProofContext.read_tyname ctxt c))
    42.7 -    |> syn ? NameSpace.base_name
    42.8 +    |> syn ? Long_Name.base_name
    42.9      |> ML_Syntax.print_string));
   42.10  
   42.11  val _ = inline "type_name" (type_ false);
    43.1 --- a/src/Pure/Proof/extraction.ML	Sun Mar 08 17:19:15 2009 +0100
    43.2 +++ b/src/Pure/Proof/extraction.ML	Sun Mar 08 17:26:14 2009 +0100
    43.3 @@ -119,7 +119,7 @@
    43.4  
    43.5  val chtype = change_type o SOME;
    43.6  
    43.7 -fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs));
    43.8 +fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs));
    43.9  fun corr_name s vs = extr_name s vs ^ "_correctness";
   43.10  
   43.11  fun msg d s = priority (Symbol.spaces d ^ s);
    44.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Mar 08 17:19:15 2009 +0100
    44.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Mar 08 17:26:14 2009 +0100
    44.3 @@ -97,16 +97,16 @@
    44.4      fun prf_of [] (Bound i) = PBound i
    44.5        | prf_of Ts (Const (s, Type ("proof", _))) =
    44.6            change_type (if ty then SOME Ts else NONE)
    44.7 -            (case NameSpace.explode s of
    44.8 +            (case Long_Name.explode s of
    44.9                 "axm" :: xs =>
   44.10                   let
   44.11 -                   val name = NameSpace.implode xs;
   44.12 +                   val name = Long_Name.implode xs;
   44.13                     val prop = (case AList.lookup (op =) axms name of
   44.14                         SOME prop => prop
   44.15                       | NONE => error ("Unknown axiom " ^ quote name))
   44.16                   in PAxm (name, prop, NONE) end
   44.17               | "thm" :: xs =>
   44.18 -                 let val name = NameSpace.implode xs;
   44.19 +                 let val name = Long_Name.implode xs;
   44.20                   in (case AList.lookup (op =) thms name of
   44.21                       SOME thm => fst (strip_combt (Thm.proof_of thm))
   44.22                     | NONE => error ("Unknown theorem " ^ quote name))
   44.23 @@ -147,12 +147,12 @@
   44.24    [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
   44.25  
   44.26  fun term_of _ (PThm (_, ((name, _, NONE), _))) =
   44.27 -      Const (NameSpace.append "thm" name, proofT)
   44.28 +      Const (Long_Name.append "thm" name, proofT)
   44.29    | term_of _ (PThm (_, ((name, _, SOME Ts), _))) =
   44.30 -      mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
   44.31 -  | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   44.32 +      mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT))
   44.33 +  | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT)
   44.34    | term_of _ (PAxm (name, _, SOME Ts)) =
   44.35 -      mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT))
   44.36 +      mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT))
   44.37    | term_of _ (PBound i) = Bound i
   44.38    | term_of Ts (Abst (s, opT, prf)) =
   44.39        let val T = the_default dummyT opT
   44.40 @@ -183,7 +183,7 @@
   44.41      val thy' = thy
   44.42        |> add_proof_syntax
   44.43        |> add_proof_atom_consts
   44.44 -        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names);
   44.45 +        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
   44.46    in
   44.47      (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
   44.48    end;
   44.49 @@ -195,7 +195,7 @@
   44.50      val ctxt = thy
   44.51        |> add_proof_syntax
   44.52        |> add_proof_atom_consts
   44.53 -        (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names)
   44.54 +        (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names)
   44.55        |> ProofContext.init
   44.56        |> ProofContext.allow_dummies
   44.57        |> ProofContext.set_mode ProofContext.mode_schematic;
   44.58 @@ -219,7 +219,7 @@
   44.59    in
   44.60      add_proof_syntax #>
   44.61      add_proof_atom_consts
   44.62 -      (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names)
   44.63 +      (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names)
   44.64    end;
   44.65  
   44.66  fun proof_of full thm =
    45.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 08 17:19:15 2009 +0100
    45.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 08 17:26:14 2009 +0100
    45.3 @@ -543,8 +543,8 @@
    45.4          fun setids t = issue_pgip (Setids {idtables = [t]})
    45.5  
    45.6          (* fake one-level nested "subtheories" by picking apart names. *)
    45.7 -        val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy
    45.8 -        fun thy_prefix s = case space_explode NameSpace.separator s of
    45.9 +        val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy
   45.10 +        fun thy_prefix s = case Long_Name.explode s of
   45.11                                      x::_::_ => SOME x  (* String.find? *)
   45.12                                    | _ => NONE
   45.13          fun subthys_of_thy s =
   45.14 @@ -553,7 +553,7 @@
   45.15          fun subthms_of_thy thy =
   45.16              (case thy_prefix thy of
   45.17                   NONE => immed_thms_of_thy thy
   45.18 -               | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy))
   45.19 +               | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy))
   45.20                                      (thms_of_thy prf))
   45.21      in
   45.22          case (thyname,objtype) of
   45.23 @@ -642,7 +642,7 @@
   45.24          val topthy = Toplevel.theory_of o Isar.state
   45.25  
   45.26          fun splitthy id =
   45.27 -            let val comps = NameSpace.explode id
   45.28 +            let val comps = Long_Name.explode id
   45.29              in case comps of
   45.30                     (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
   45.31                   | [plainid] => (topthy(),plainid)
    46.1 --- a/src/Pure/Syntax/syntax.ML	Sun Mar 08 17:19:15 2009 +0100
    46.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Mar 08 17:26:14 2009 +0100
    46.3 @@ -301,7 +301,7 @@
    46.4        lexicon =
    46.5          if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon,
    46.6        gram = if changed then Parser.extend_gram gram xprods else gram,
    46.7 -      consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2),
    46.8 +      consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2),
    46.9        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
   46.10        parse_ast_trtab =
   46.11          update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
   46.12 @@ -607,7 +607,7 @@
   46.13  
   46.14      fun constify (ast as Ast.Constant _) = ast
   46.15        | constify (ast as Ast.Variable x) =
   46.16 -          if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x
   46.17 +          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
   46.18            else ast
   46.19        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   46.20  
    47.1 --- a/src/Pure/Syntax/type_ext.ML	Sun Mar 08 17:19:15 2009 +0100
    47.2 +++ b/src/Pure/Syntax/type_ext.ML	Sun Mar 08 17:26:14 2009 +0100
    47.3 @@ -129,7 +129,7 @@
    47.4            (case (map_free a, map_const a) of
    47.5              (SOME x, _) => Free (x, map_type T)
    47.6            | (_, (true, c)) => Const (c, map_type T)
    47.7 -          | (_, (false, c)) => (if NameSpace.is_qualified c then Const else Free) (c, map_type T))
    47.8 +          | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T))
    47.9        | decode (Var (xi, T)) = Var (xi, map_type T)
   47.10        | decode (t as Bound _) = t;
   47.11    in decode tm end;
    48.1 --- a/src/Pure/Thy/thm_deps.ML	Sun Mar 08 17:19:15 2009 +0100
    48.2 +++ b/src/Pure/Thy/thm_deps.ML	Sun Mar 08 17:26:14 2009 +0100
    48.3 @@ -20,7 +20,7 @@
    48.4      fun add_dep ("", _, _) = I
    48.5        | add_dep (name, _, PBody {thms = thms', ...}) =
    48.6            let
    48.7 -            val prefix = #1 (Library.split_last (NameSpace.explode name));
    48.8 +            val prefix = #1 (Library.split_last (Long_Name.explode name));
    48.9              val session =
   48.10                (case prefix of
   48.11                  a :: _ =>
   48.12 @@ -33,7 +33,7 @@
   48.13                 | _ => ["global"]);
   48.14              val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
   48.15              val entry =
   48.16 -              {name = NameSpace.base_name name,
   48.17 +              {name = Long_Name.base_name name,
   48.18                 ID = name,
   48.19                 dir = space_implode "/" (session @ prefix),
   48.20                 unfold = false,
    49.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 08 17:19:15 2009 +0100
    49.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 08 17:26:14 2009 +0100
    49.3 @@ -279,7 +279,7 @@
    49.4  
    49.5  val index_ord = option_ord (K EQUAL);
    49.6  val hidden_ord = bool_ord o pairself NameSpace.is_hidden;
    49.7 -val qual_ord = int_ord o pairself (length o NameSpace.explode);
    49.8 +val qual_ord = int_ord o pairself (length o Long_Name.explode);
    49.9  val txt_ord = int_ord o pairself size;
   49.10  
   49.11  fun nicer_name (x, i) (y, j) =
    50.1 --- a/src/Pure/axclass.ML	Sun Mar 08 17:19:15 2009 +0100
    50.2 +++ b/src/Pure/axclass.ML	Sun Mar 08 17:26:14 2009 +0100
    50.3 @@ -158,7 +158,7 @@
    50.4  
    50.5  (* maintain instances *)
    50.6  
    50.7 -fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a;
    50.8 +fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a;
    50.9  
   50.10  val get_instances = #1 o #2 o AxClassData.get;
   50.11  val map_instances = AxClassData.map o apsnd o apfst;
   50.12 @@ -366,7 +366,7 @@
   50.13        | NONE => error ("Illegal type for instantiation of class parameter: "
   50.14          ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T));
   50.15      val name_inst = instance_name (tyco, class) ^ "_inst";
   50.16 -    val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco;
   50.17 +    val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco;
   50.18      val T' = Type.strip_sorts T;
   50.19    in
   50.20      thy
   50.21 @@ -390,7 +390,7 @@
   50.22      val SOME tyco = inst_tyco_of thy (c, T);
   50.23      val (c', eq) = get_inst_param thy (c, tyco);
   50.24      val prop = Logic.mk_equals (Const (c', T), t);
   50.25 -    val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name;
   50.26 +    val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name;
   50.27    in
   50.28      thy
   50.29      |> Thm.add_def false false (Binding.name name', prop)
    51.1 --- a/src/Pure/codegen.ML	Sun Mar 08 17:19:15 2009 +0100
    51.2 +++ b/src/Pure/codegen.ML	Sun Mar 08 17:26:14 2009 +0100
    51.3 @@ -378,7 +378,7 @@
    51.4              | (true, "isup") => "" :: check_str zs
    51.5              | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs)
    51.6          | (ys, zs) => implode ys :: check_str zs);
    51.7 -    val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s))
    51.8 +    val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s))
    51.9    in
   51.10      if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s'
   51.11    end;
   51.12 @@ -388,8 +388,8 @@
   51.13      fun find_name [] = sys_error "mk_long_id"
   51.14        | find_name (ys :: yss) =
   51.15            let
   51.16 -            val s' = NameSpace.implode ys
   51.17 -            val s'' = NameSpace.append module s'
   51.18 +            val s' = Long_Name.implode ys
   51.19 +            val s'' = Long_Name.append module s'
   51.20            in case Symtab.lookup used s'' of
   51.21                NONE => ((module, s'),
   51.22                  (Symtab.update_new (s, (module, s')) tab,
   51.23 @@ -397,7 +397,7 @@
   51.24              | SOME _ => find_name yss
   51.25            end
   51.26    in case Symtab.lookup tab s of
   51.27 -      NONE => find_name (Library.suffixes1 (NameSpace.explode s))
   51.28 +      NONE => find_name (Library.suffixes1 (Long_Name.explode s))
   51.29      | SOME name => (name, p)
   51.30    end;
   51.31  
    52.1 --- a/src/Pure/consts.ML	Sun Mar 08 17:19:15 2009 +0100
    52.2 +++ b/src/Pure/consts.ML	Sun Mar 08 17:26:14 2009 +0100
    52.3 @@ -117,7 +117,7 @@
    52.4  fun syntax consts (c, mx) =
    52.5    let
    52.6      val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg;
    52.7 -    val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c;
    52.8 +    val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c;
    52.9    in (c', T, mx) end;
   52.10  
   52.11  fun syntax_name consts c = #1 (syntax consts (c, NoSyn));
    53.1 --- a/src/Pure/logic.ML	Sun Mar 08 17:19:15 2009 +0100
    53.2 +++ b/src/Pure/logic.ML	Sun Mar 08 17:26:14 2009 +0100
    53.3 @@ -230,7 +230,7 @@
    53.4  (* class relations *)
    53.5  
    53.6  fun name_classrel (c1, c2) =
    53.7 -  NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2;
    53.8 +  Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2;
    53.9  
   53.10  fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2);
   53.11  
   53.12 @@ -243,8 +243,8 @@
   53.13  (* type arities *)
   53.14  
   53.15  fun name_arities (t, _, S) =
   53.16 -  let val b = NameSpace.base_name t
   53.17 -  in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end;
   53.18 +  let val b = Long_Name.base_name t
   53.19 +  in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end;
   53.20  
   53.21  fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c]));
   53.22  
    54.1 --- a/src/Pure/old_term.ML	Sun Mar 08 17:19:15 2009 +0100
    54.2 +++ b/src/Pure/old_term.ML	Sun Mar 08 17:26:14 2009 +0100
    54.3 @@ -39,7 +39,7 @@
    54.4  
    54.5  (*Accumulates the names in the term, suppressing duplicates.
    54.6    Includes Frees and Consts.  For choosing unambiguous bound var names.*)
    54.7 -fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs
    54.8 +fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs
    54.9    | add_term_names (Free(a,_), bs) = insert (op =) a bs
   54.10    | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   54.11    | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
    55.1 --- a/src/Pure/primitive_defs.ML	Sun Mar 08 17:19:15 2009 +0100
    55.2 +++ b/src/Pure/primitive_defs.ML	Sun Mar 08 17:26:14 2009 +0100
    55.3 @@ -81,7 +81,7 @@
    55.4  fun mk_defpair (lhs, rhs) =
    55.5    (case Term.head_of lhs of
    55.6      Const (name, _) =>
    55.7 -      (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    55.8 +      (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
    55.9    | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
   55.10  
   55.11  end;
    56.1 --- a/src/Pure/sign.ML	Sun Mar 08 17:19:15 2009 +0100
    56.2 +++ b/src/Pure/sign.ML	Sun Mar 08 17:26:14 2009 +0100
    56.3 @@ -355,7 +355,7 @@
    56.4  fun check_vars (t $ u) = (check_vars t; check_vars u)
    56.5    | check_vars (Abs (_, _, t)) = check_vars t
    56.6    | check_vars (Free (x, _)) =
    56.7 -      if NameSpace.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
    56.8 +      if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
    56.9    | check_vars (Var (xi as (_, i), _)) =
   56.10        if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
   56.11    | check_vars _ = ();
    57.1 --- a/src/Pure/term.ML	Sun Mar 08 17:19:15 2009 +0100
    57.2 +++ b/src/Pure/term.ML	Sun Mar 08 17:26:14 2009 +0100
    57.3 @@ -490,7 +490,7 @@
    57.4  
    57.5  fun declare_term_names tm =
    57.6    fold_aterms
    57.7 -    (fn Const (a, _) => Name.declare (NameSpace.base_name a)
    57.8 +    (fn Const (a, _) => Name.declare (Long_Name.base_name a)
    57.9        | Free (a, _) => Name.declare a
   57.10        | _ => I) tm #>
   57.11    fold_types declare_typ_names tm;
   57.12 @@ -721,7 +721,7 @@
   57.13  fun lambda v t =
   57.14    let val x =
   57.15      (case v of
   57.16 -      Const (x, _) => NameSpace.base_name x
   57.17 +      Const (x, _) => Long_Name.base_name x
   57.18      | Free (x, _) => x
   57.19      | Var ((x, _), _) => x
   57.20      | _ => Name.uu)
    58.1 --- a/src/Tools/code/code_haskell.ML	Sun Mar 08 17:19:15 2009 +0100
    58.2 +++ b/src/Tools/code/code_haskell.ML	Sun Mar 08 17:26:14 2009 +0100
    58.3 @@ -34,7 +34,7 @@
    58.4  fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
    58.5      init_syms deresolve is_cons contr_classparam_typs deriving_show =
    58.6    let
    58.7 -    val deresolve_base = NameSpace.base_name o deresolve;
    58.8 +    val deresolve_base = Long_Name.base_name o deresolve;
    58.9      fun class_name class = case syntax_class class
   58.10       of NONE => deresolve class
   58.11        | SOME class => class;
   58.12 @@ -143,7 +143,7 @@
   58.13                  @ str "="
   58.14                  :: str "error"
   58.15                  @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
   58.16 -                    o NameSpace.base_name o NameSpace.qualifier) name
   58.17 +                    o Long_Name.base_name o Long_Name.qualifier) name
   58.18                )
   58.19              ]
   58.20            end
   58.21 @@ -155,7 +155,7 @@
   58.22                let
   58.23                  val consts = map_filter
   58.24                    (fn c => if (is_some o syntax_const) c
   58.25 -                    then NONE else (SOME o NameSpace.base_name o deresolve) c)
   58.26 +                    then NONE else (SOME o Long_Name.base_name o deresolve) c)
   58.27                      ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   58.28                  val vars = init_syms
   58.29                    |> Code_Name.intro_vars consts
   58.30 @@ -255,7 +255,7 @@
   58.31                    let
   58.32                      val (c_inst_name, (_, tys)) = c_inst;
   58.33                      val const = if (is_some o syntax_const) c_inst_name
   58.34 -                      then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name;
   58.35 +                      then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name;
   58.36                      val proto_rhs = Code_Thingol.eta_expand k (c_inst, []);
   58.37                      val (vs, rhs) = unfold_abs_pure proto_rhs;
   58.38                      val vars = init_syms
   58.39 @@ -313,11 +313,11 @@
   58.40            | Code_Thingol.Classinst _ => pair base;
   58.41          fun add_stmt' base' = case stmt
   58.42           of Code_Thingol.Datatypecons _ =>
   58.43 -              cons (name, (NameSpace.append module_name' base', NONE))
   58.44 +              cons (name, (Long_Name.append module_name' base', NONE))
   58.45            | Code_Thingol.Classrel _ => I
   58.46            | Code_Thingol.Classparam _ =>
   58.47 -              cons (name, (NameSpace.append module_name' base', NONE))
   58.48 -          | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
   58.49 +              cons (name, (Long_Name.append module_name' base', NONE))
   58.50 +          | _ => cons (name, (Long_Name.append module_name' base', SOME stmt));
   58.51        in
   58.52          Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
   58.53                (apfst (fold (insert (op = : string * string -> bool)) deps))
   58.54 @@ -360,7 +360,7 @@
   58.55      val reserved_names = Code_Name.make_vars reserved_names;
   58.56      fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
   58.57        syntax_class syntax_tyco syntax_const reserved_names
   58.58 -      (if qualified then deresolver else NameSpace.base_name o deresolver)
   58.59 +      (if qualified then deresolver else Long_Name.base_name o deresolver)
   58.60        is_cons contr_classparam_typs
   58.61        (if string_classes then deriving_show else K false);
   58.62      fun pr_module name content =
   58.63 @@ -379,10 +379,10 @@
   58.64            |> map_filter (try deresolver);
   58.65          val qualified = is_none module_name andalso
   58.66            map deresolver stmt_names @ deps'
   58.67 -          |> map NameSpace.base_name
   58.68 +          |> map Long_Name.base_name
   58.69            |> has_duplicates (op =);
   58.70          val imports = deps'
   58.71 -          |> map NameSpace.qualifier
   58.72 +          |> map Long_Name.qualifier
   58.73            |> distinct (op =);
   58.74          fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";");
   58.75          val pr_import_module = str o (if qualified
   58.76 @@ -413,7 +413,7 @@
   58.77          val filename = case modlname
   58.78           of "" => Path.explode "Main.hs"
   58.79            | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
   58.80 -                o NameSpace.explode) modlname;
   58.81 +                o Long_Name.explode) modlname;
   58.82          val pathname = Path.append destination filename;
   58.83          val _ = File.mkdir (Path.dir pathname);
   58.84        in File.write pathname
    59.1 --- a/src/Tools/code/code_ml.ML	Sun Mar 08 17:19:15 2009 +0100
    59.2 +++ b/src/Tools/code/code_ml.ML	Sun Mar 08 17:26:14 2009 +0100
    59.3 @@ -46,8 +46,8 @@
    59.4  fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
    59.5    let
    59.6      val pr_label_classrel = translate_string (fn "." => "__" | c => c)
    59.7 -      o NameSpace.qualifier;
    59.8 -    val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier;
    59.9 +      o Long_Name.qualifier;
   59.10 +    val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier;
   59.11      fun pr_dicts fxy ds =
   59.12        let
   59.13          fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_"
   59.14 @@ -163,7 +163,7 @@
   59.15      fun pr_stmt (MLExc (name, n)) =
   59.16            let
   59.17              val exc_str =
   59.18 -              (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
   59.19 +              (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
   59.20            in
   59.21              concat (
   59.22                str (if n = 0 then "val" else "fun")
   59.23 @@ -179,7 +179,7 @@
   59.24            let
   59.25              val consts = map_filter
   59.26                (fn c => if (is_some o syntax_const) c
   59.27 -                then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.28 +                then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.29                  (Code_Thingol.fold_constnames (insert (op =)) t []);
   59.30              val vars = reserved_names
   59.31                |> Code_Name.intro_vars consts;
   59.32 @@ -204,7 +204,7 @@
   59.33                    let
   59.34                      val consts = map_filter
   59.35                        (fn c => if (is_some o syntax_const) c
   59.36 -                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.37 +                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.38                          ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   59.39                      val vars = reserved_names
   59.40                        |> Code_Name.intro_vars consts
   59.41 @@ -473,7 +473,7 @@
   59.42      fun pr_stmt (MLExc (name, n)) =
   59.43            let
   59.44              val exc_str =
   59.45 -              (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name;
   59.46 +              (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name;
   59.47            in
   59.48              concat (
   59.49                str "let"
   59.50 @@ -488,7 +488,7 @@
   59.51            let
   59.52              val consts = map_filter
   59.53                (fn c => if (is_some o syntax_const) c
   59.54 -                then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.55 +                then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.56                  (Code_Thingol.fold_constnames (insert (op =)) t []);
   59.57              val vars = reserved_names
   59.58                |> Code_Name.intro_vars consts;
   59.59 @@ -508,7 +508,7 @@
   59.60                let
   59.61                  val consts = map_filter
   59.62                    (fn c => if (is_some o syntax_const) c
   59.63 -                    then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.64 +                    then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.65                      ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   59.66                  val vars = reserved_names
   59.67                    |> Code_Name.intro_vars consts
   59.68 @@ -524,7 +524,7 @@
   59.69                    let
   59.70                      val consts = map_filter
   59.71                        (fn c => if (is_some o syntax_const) c
   59.72 -                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.73 +                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.74                          ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
   59.75                      val vars = reserved_names
   59.76                        |> Code_Name.intro_vars consts
   59.77 @@ -552,7 +552,7 @@
   59.78                    let
   59.79                      val consts = map_filter
   59.80                        (fn c => if (is_some o syntax_const) c
   59.81 -                        then NONE else (SOME o NameSpace.base_name o deresolve) c)
   59.82 +                        then NONE else (SOME o Long_Name.base_name o deresolve) c)
   59.83                          ((fold o Code_Thingol.fold_constnames)
   59.84                            (insert (op =)) (map (snd o fst) eqs) []);
   59.85                      val vars = reserved_names
   59.86 @@ -860,7 +860,7 @@
   59.87                ^ commas (map labelled_name names)
   59.88                ^ "\n"
   59.89                ^ commas module_names);
   59.90 -        val module_name_path = NameSpace.explode module_name;
   59.91 +        val module_name_path = Long_Name.explode module_name;
   59.92          fun add_dep name name' =
   59.93            let
   59.94              val module_name' = (mk_name_module o fst o Code_Name.dest_name) name';
   59.95 @@ -868,7 +868,7 @@
   59.96              map_node module_name_path (Graph.add_edge (name, name'))
   59.97            else let
   59.98              val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =)
   59.99 -              (module_name_path, NameSpace.explode module_name');
  59.100 +              (module_name_path, Long_Name.explode module_name');
  59.101            in
  59.102              map_node common
  59.103                (fn node => Graph.add_edge_acyclic (diff1, diff2) node
  59.104 @@ -892,7 +892,7 @@
  59.105      fun deresolver prefix name = 
  59.106        let
  59.107          val module_name = (fst o Code_Name.dest_name) name;
  59.108 -        val module_name' = (NameSpace.explode o mk_name_module) module_name;
  59.109 +        val module_name' = (Long_Name.explode o mk_name_module) module_name;
  59.110          val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
  59.111          val stmt_name =
  59.112            nodes
  59.113 @@ -901,7 +901,7 @@
  59.114            |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
  59.115                 | Dummy stmt_name => stmt_name);
  59.116        in
  59.117 -        NameSpace.implode (remainder @ [stmt_name])
  59.118 +        Long_Name.implode (remainder @ [stmt_name])
  59.119        end handle Graph.UNDEF _ =>
  59.120          error ("Unknown statement name: " ^ labelled_name name);
  59.121    in (deresolver, nodes) end;
  59.122 @@ -1011,7 +1011,7 @@
  59.123    let
  59.124      val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
  59.125      val (raw_ml_code, consts_map) = Lazy.force acc_code;
  59.126 -    val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
  59.127 +    val const'' = Long_Name.append (Long_Name.append struct_name struct_code_name)
  59.128        ((the o AList.lookup (op =) consts_map) const);
  59.129      val ml_code = if is_first then "\nstructure " ^ struct_code_name
  59.130          ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
    60.1 --- a/src/Tools/code/code_name.ML	Sun Mar 08 17:19:15 2009 +0100
    60.2 +++ b/src/Tools/code/code_name.ML	Sun Mar 08 17:26:14 2009 +0100
    60.3 @@ -39,7 +39,7 @@
    60.4  val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    60.5  
    60.6  val dest_name =
    60.7 -  apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
    60.8 +  apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode;
    60.9  
   60.10  
   60.11  (** purification **)
   60.12 @@ -80,7 +80,7 @@
   60.13    #> Symbol.scanner "Malformed name"
   60.14        (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular))
   60.15    #> implode
   60.16 -  #> NameSpace.explode
   60.17 +  #> Long_Name.explode
   60.18    #> map (purify_name true false);
   60.19  
   60.20  (*FIMXE non-canonical function treating non-canonical names*)
   60.21 @@ -101,11 +101,11 @@
   60.22  
   60.23  fun check_modulename mn =
   60.24    let
   60.25 -    val mns = NameSpace.explode mn;
   60.26 +    val mns = Long_Name.explode mn;
   60.27      val mns' = map (purify_name true false) mns;
   60.28    in
   60.29      if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n"
   60.30 -      ^ "perhaps try " ^ quote (NameSpace.implode mns'))
   60.31 +      ^ "perhaps try " ^ quote (Long_Name.implode mns'))
   60.32    end;
   60.33  
   60.34  
   60.35 @@ -155,11 +155,11 @@
   60.36      fun mk_alias name = case module_alias name
   60.37       of SOME name' => name'
   60.38        | NONE => name
   60.39 -          |> NameSpace.explode
   60.40 +          |> Long_Name.explode
   60.41            |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
   60.42 -          |> NameSpace.implode;
   60.43 +          |> Long_Name.implode;
   60.44      fun mk_prefix name = case module_prefix
   60.45 -     of SOME module_prefix => NameSpace.append module_prefix name
   60.46 +     of SOME module_prefix => Long_Name.append module_prefix name
   60.47        | NONE => name;
   60.48      val tab =
   60.49        Symtab.empty
    61.1 --- a/src/Tools/code/code_thingol.ML	Sun Mar 08 17:19:15 2009 +0100
    61.2 +++ b/src/Tools/code/code_thingol.ML	Sun Mar 08 17:26:14 2009 +0100
    61.3 @@ -243,18 +243,18 @@
    61.4      let
    61.5        val prefix = get_thyname thy name;
    61.6        val base = (Code_Name.purify_base true o get_basename) name;
    61.7 -    in NameSpace.append prefix base end;
    61.8 +    in Long_Name.append prefix base end;
    61.9  in
   61.10  
   61.11 -fun namify_class thy = namify thy NameSpace.base_name thyname_of_class;
   61.12 +fun namify_class thy = namify thy Long_Name.base_name thyname_of_class;
   61.13  fun namify_classrel thy = namify thy (fn (class1, class2) => 
   61.14 -  NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst);
   61.15 +  Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst);
   61.16    (*order fits nicely with composed projections*)
   61.17  fun namify_tyco thy "fun" = "Pure.fun"
   61.18 -  | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco;
   61.19 +  | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco;
   61.20  fun namify_instance thy = namify thy (fn (class, tyco) => 
   61.21 -  NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance;
   61.22 -fun namify_const thy = namify thy NameSpace.base_name thyname_of_const;
   61.23 +  Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance;
   61.24 +fun namify_const thy = namify thy Long_Name.base_name thyname_of_const;
   61.25  
   61.26  end; (* local *)
   61.27  
   61.28 @@ -327,7 +327,7 @@
   61.29  val suffix_const = "const";
   61.30  
   61.31  fun add_suffix nsp NONE = NONE
   61.32 -  | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp);
   61.33 +  | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp);
   61.34  
   61.35  in
   61.36  
    62.1 --- a/src/ZF/Tools/datatype_package.ML	Sun Mar 08 17:19:15 2009 +0100
    62.2 +++ b/src/ZF/Tools/datatype_package.ML	Sun Mar 08 17:26:14 2009 +0100
    62.3 @@ -74,7 +74,7 @@
    62.4                     Syntax.string_of_term_global thy t);
    62.5  
    62.6    val rec_names = map (#1 o dest_Const) rec_hds
    62.7 -  val rec_base_names = map NameSpace.base_name rec_names
    62.8 +  val rec_base_names = map Long_Name.base_name rec_names
    62.9    val big_rec_base_name = space_implode "_" rec_base_names
   62.10  
   62.11    val thy_path = thy |> Sign.add_path big_rec_base_name
    63.1 --- a/src/ZF/Tools/induct_tacs.ML	Sun Mar 08 17:19:15 2009 +0100
    63.2 +++ b/src/ZF/Tools/induct_tacs.ML	Sun Mar 08 17:26:14 2009 +0100
    63.3 @@ -157,7 +157,7 @@
    63.4  
    63.5    in
    63.6      thy
    63.7 -    |> Sign.add_path (NameSpace.base_name big_rec_name)
    63.8 +    |> Sign.add_path (Long_Name.base_name big_rec_name)
    63.9      |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd
   63.10      |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy))
   63.11      |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy))
    64.1 --- a/src/ZF/Tools/inductive_package.ML	Sun Mar 08 17:19:15 2009 +0100
    64.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Mar 08 17:26:14 2009 +0100
    64.3 @@ -80,7 +80,7 @@
    64.4    val rec_names = map (#1 o dest_Const) rec_hds
    64.5    and (Const(_,recT),rec_params) = strip_comb (hd rec_tms);
    64.6  
    64.7 -  val rec_base_names = map NameSpace.base_name rec_names;
    64.8 +  val rec_base_names = map Long_Name.base_name rec_names;
    64.9    val dummy = assert_all Syntax.is_identifier rec_base_names
   64.10      (fn a => "Base name of recursive set not an identifier: " ^ a);
   64.11  
   64.12 @@ -377,7 +377,7 @@
   64.13         mutual recursion to invariably be a disjoint sum.*)
   64.14       fun mk_predpair rec_tm =
   64.15         let val rec_name = (#1 o dest_Const o head_of) rec_tm
   64.16 -           val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name,
   64.17 +           val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name,
   64.18                              elem_factors ---> FOLogic.oT)
   64.19             val qconcl =
   64.20               List.foldr FOLogic.mk_all
    65.1 --- a/src/ZF/Tools/primrec_package.ML	Sun Mar 08 17:19:15 2009 +0100
    65.2 +++ b/src/ZF/Tools/primrec_package.ML	Sun Mar 08 17:26:14 2009 +0100
    65.3 @@ -139,7 +139,7 @@
    65.4      (** make definition **)
    65.5  
    65.6      (*the recursive argument*)
    65.7 -    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name),
    65.8 +    val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name),
    65.9                          Ind_Syntax.iT)
   65.10  
   65.11      val def_tm = Logic.mk_equals
   65.12 @@ -153,7 +153,7 @@
   65.13              writeln ("primrec def:\n" ^
   65.14                       Syntax.string_of_term_global thy def_tm)
   65.15        else();
   65.16 -      (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def",
   65.17 +      (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def",
   65.18         def_tm)
   65.19    end;
   65.20  
   65.21 @@ -168,7 +168,7 @@
   65.22      val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns);
   65.23  
   65.24      val ([def_thm], thy1) = thy
   65.25 -      |> Sign.add_path (NameSpace.base_name fname)
   65.26 +      |> Sign.add_path (Long_Name.base_name fname)
   65.27        |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)];
   65.28  
   65.29      val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)