# HG changeset patch # User wenzelm # Date 1236529574 -3600 # Node ID 577edc39b501ead0a97f6d017dc5b34f7adcbd29 # Parent 9b8d9b6ef80378d0bb6e3012c41312768aa222a6 moved basic algebra of long names from structure NameSpace to Long_Name; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Import/hol4rews.ML Sun Mar 08 17:26:14 2009 +0100 @@ -495,7 +495,7 @@ if internal then let - val paths = NameSpace.explode isa + val paths = Long_Name.explode isa val i = Library.drop(length paths - 2,paths) in case i of @@ -549,10 +549,10 @@ fun gen2replay in_thy out_thy s = let - val ss = NameSpace.explode s + val ss = Long_Name.explode s in if (hd ss = in_thy) then - NameSpace.implode (out_thy::(tl ss)) + Long_Name.implode (out_thy::(tl ss)) else s end diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sun Mar 08 17:26:14 2009 +0100 @@ -72,7 +72,7 @@ let val thy = theory_of_thm thm; (* the parsing function returns a qualified name, we get back the base name *) - val atom_basename = NameSpace.base_name atom_name; + val atom_basename = Long_Name.base_name atom_name; val goal = List.nth(prems_of thm, i-1); val ps = Logic.strip_params goal; val Ts = rev (map snd ps); @@ -159,7 +159,7 @@ NONE => all_tac thm | SOME atom_name => let - val atom_basename = NameSpace.base_name atom_name; + val atom_basename = Long_Name.base_name atom_name; val pt_name_inst = get_dyn_thm thy ("pt_"^atom_basename^"_inst") atom_basename; val at_name_inst = get_dyn_thm thy ("at_"^atom_basename^"_inst") atom_basename; fun inst_fresh vars params i st = diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive.ML Sun Mar 08 17:26:14 2009 +0100 @@ -199,7 +199,7 @@ val atomTs = distinct op = (maps (map snd o #2) prems); val ind_sort = if null atomTs then HOLogic.typeS else Sign.certify_sort thy (map (fn T => Sign.intern_class thy - ("fs_" ^ NameSpace.base_name (fst (dest_Type T)))) atomTs); + ("fs_" ^ Long_Name.base_name (fst (dest_Type T)))) atomTs); val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); @@ -273,7 +273,7 @@ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn aT => PureThy.get_thm thy - ("pt_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "2")) atomTs; + ("pt_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "2")) atomTs; val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], @@ -281,7 +281,7 @@ val fresh_bij = PureThy.get_thms thy "fresh_bij"; val perm_bij = PureThy.get_thms thy "perm_bij"; val fs_atoms = map (fn aT => PureThy.get_thm thy - ("fs_" ^ NameSpace.base_name (fst (dest_Type aT)) ^ "1")) atomTs; + ("fs_" ^ Long_Name.base_name (fst (dest_Type aT)) ^ "1")) atomTs; val exists_fresh' = PureThy.get_thms thy "exists_fresh'"; val fresh_atm = PureThy.get_thms thy "fresh_atm"; val swap_simps = PureThy.get_thms thy "swap_simps"; @@ -545,7 +545,7 @@ ctxt'' |> Proof.theorem_i NONE (fn thss => fn ctxt => let - val rec_name = space_implode "_" (map NameSpace.base_name names); + val rec_name = space_implode "_" (map Long_Name.base_name names); val rec_qualified = Binding.qualify false rec_name; val ind_case_names = RuleCases.case_names induct_cases; val induct_cases' = InductivePackage.partition_rules' raw_induct @@ -575,7 +575,7 @@ Attrib.internal (K (RuleCases.consumes 1))]), strong_inducts) |> snd |> LocalTheory.notes Thm.theoremK (map (fn ((name, elim), (_, cases)) => - ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "strong_cases"), + ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "strong_cases"), [Attrib.internal (K (RuleCases.case_names (map snd cases))), Attrib.internal (K (RuleCases.consumes 1))]), [([elim], [])])) (strong_cases ~~ induct_cases')) |> snd @@ -665,7 +665,7 @@ in ctxt |> LocalTheory.notes Thm.theoremK (map (fn (name, ths) => - ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "eqvt"), + ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "eqvt"), [Attrib.internal (K NominalThmDecls.eqvt_add)]), [(ths, [])])) (names ~~ transp thss)) |> snd end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sun Mar 08 17:26:14 2009 +0100 @@ -229,7 +229,7 @@ val atoms = map (fst o dest_Type) atomTs; val ind_sort = if null atomTs then HOLogic.typeS else Sign.certify_sort thy (map (fn a => Sign.intern_class thy - ("fs_" ^ NameSpace.base_name a)) atoms); + ("fs_" ^ Long_Name.base_name a)) atoms); val ([fs_ctxt_tyname], _) = Name.variants ["'n"] (Variable.names_of ctxt'); val ([fs_ctxt_name], ctxt'') = Variable.variant_fixes ["z"] ctxt'; val fsT = TFree (fs_ctxt_tyname, ind_sort); @@ -296,7 +296,7 @@ val perm_pi_simp = PureThy.get_thms thy "perm_pi_simp"; val pt2_atoms = map (fn a => PureThy.get_thm thy - ("pt_" ^ NameSpace.base_name a ^ "2")) atoms; + ("pt_" ^ Long_Name.base_name a ^ "2")) atoms; val eqvt_ss = Simplifier.theory_context thy HOL_basic_ss addsimps (eqvt_thms @ perm_pi_simp @ pt2_atoms) addsimprocs [mk_perm_bool_simproc ["Fun.id"], @@ -324,7 +324,7 @@ val atom = fst (dest_Type T); val {at_inst, ...} = NominalAtoms.the_atom_info thy atom; val fs_atom = PureThy.get_thm thy - ("fs_" ^ NameSpace.base_name atom ^ "1"); + ("fs_" ^ Long_Name.base_name atom ^ "1"); val avoid_th = Drule.instantiate' [SOME (ctyp_of thy (fastype_of p))] [SOME (cterm_of thy p)] ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding}); @@ -452,7 +452,7 @@ ctxt'' |> Proof.theorem_i NONE (fn thss => fn ctxt => let - val rec_name = space_implode "_" (map NameSpace.base_name names); + val rec_name = space_implode "_" (map Long_Name.base_name names); val rec_qualified = Binding.qualify false rec_name; val ind_case_names = RuleCases.case_names induct_cases; val induct_cases' = InductivePackage.partition_rules' raw_induct diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -49,9 +49,9 @@ fun dt_cases (descr: descr) (_, args, constrs) = let - fun the_bname i = NameSpace.base_name (#1 (valOf (AList.lookup (op =) descr i))); + fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i))); val bnames = map the_bname (distinct op = (List.concat (map dt_recs args))); - in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end; + in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; fun induct_cases descr = @@ -364,7 +364,7 @@ val pi2 = Free ("pi2", permT); val pt_inst = pt_inst_of thy2 a; val pt2' = pt_inst RS pt2; - val pt2_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "2") a); + val pt2_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "2") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] @@ -399,7 +399,7 @@ val pt_inst = pt_inst_of thy2 a; val pt3' = pt_inst RS pt3; val pt3_rev' = at_inst RS (pt_inst RS pt3_rev); - val pt3_ax = PureThy.get_thm thy2 (NameSpace.map_base_name (fn s => "pt_" ^ s ^ "3") a); + val pt3_ax = PureThy.get_thm thy2 (Long_Name.map_base_name (fn s => "pt_" ^ s ^ "3") a); in List.take (map standard (split_conj_thm (Goal.prove_global thy2 [] [] (augment_sort thy2 [pt_class_of thy2 a] (Logic.mk_implies @@ -665,7 +665,7 @@ asm_full_simp_tac (simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy - ("pt_" ^ NameSpace.base_name atom ^ "3")]) 1]) thy + ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy end) (Abs_inverse_thms ~~ Rep_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms); @@ -729,8 +729,8 @@ (** strips the "_Rep" in type names *) fun strip_nth_name i s = - let val xs = NameSpace.explode s; - in NameSpace.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; + let val xs = Long_Name.explode s; + in Long_Name.implode (Library.nth_map (length xs - i) (strip_suffix 4) xs) end; val (descr'', ndescr) = ListPair.unzip (List.mapPartial (fn (i, ("Nominal.noption", _, _)) => NONE @@ -799,7 +799,7 @@ val def = Logic.mk_equals (lhs, Const (abs_name, T' --> T) $ rhs); val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> T') $ lhs, rhs)); - val def_name = (NameSpace.base_name cname) ^ "_def"; + val def_name = (Long_Name.base_name cname) ^ "_def"; val ([def_thm], thy') = thy |> Sign.add_consts_i [(Binding.name cname', constrT, mx)] |> (PureThy.add_defs false o map Thm.no_attributes) [(Binding.name def_name, def)] @@ -890,7 +890,7 @@ map (fn ((cname, dts), constr_rep_thm) => let val cname = Sign.intern_const thy8 - (NameSpace.append tname (NameSpace.base_name cname)); + (Long_Name.append tname (Long_Name.base_name cname)); val permT = mk_permT (Type (atom, [])); val pi = Free ("pi", permT); @@ -946,7 +946,7 @@ if null dts then NONE else SOME let val cname = Sign.intern_const thy8 - (NameSpace.append tname (NameSpace.base_name cname)); + (Long_Name.append tname (Long_Name.base_name cname)); fun make_inj ((dts, dt), (j, args1, args2, eqs)) = let @@ -988,7 +988,7 @@ in List.concat (map (fn (cname, dts) => map (fn atom => let val cname = Sign.intern_const thy8 - (NameSpace.append tname (NameSpace.base_name cname)); + (Long_Name.append tname (Long_Name.base_name cname)); val atomT = Type (atom, []); fun process_constr ((dts, dt), (j, args1, args2)) = @@ -1101,7 +1101,7 @@ (fn _ => indtac dt_induct indnames 1 THEN ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps (abs_supp @ supp_atm @ - PureThy.get_thms thy8 ("fs_" ^ NameSpace.base_name atom ^ "1") @ + PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ List.concat supp_thms))))), length new_type_names)) end) atoms; @@ -1233,9 +1233,9 @@ val fin_set_fresh = map (fn s => at_inst_of thy9 s RS at_fin_set_fresh) dt_atoms; val pt1_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "1")) dt_atomTs; + PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "1")) dt_atomTs; val pt2_atoms = map (fn Type (s, _) => - PureThy.get_thm thy9 ("pt_" ^ NameSpace.base_name s ^ "2") RS sym) dt_atomTs; + PureThy.get_thm thy9 ("pt_" ^ Long_Name.base_name s ^ "2") RS sym) dt_atomTs; val exists_fresh' = PureThy.get_thms thy9 "exists_fresh'"; val fs_atoms = PureThy.get_thms thy9 "fin_supp"; val abs_supp = PureThy.get_thms thy9 "abs_supp"; @@ -1514,7 +1514,7 @@ (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) (map dest_Free rec_fns) (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||> - PureThy.hide_fact true (NameSpace.append (Sign.full_bname thy10 big_rec_name) "induct"); + PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct"); (** equivariance **) @@ -1560,7 +1560,7 @@ val rec_fin_supp_thms = map (fn aT => let - val name = NameSpace.base_name (fst (dest_Type aT)); + val name = Long_Name.base_name (fst (dest_Type aT)); val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); val aset = HOLogic.mk_setT aT; val finite = Const ("Finite_Set.finite", aset --> HOLogic.boolT); @@ -1599,7 +1599,7 @@ val rec_fresh_thms = map (fn ((aT, eqvt_ths), finite_prems) => let - val name = NameSpace.base_name (fst (dest_Type aT)); + val name = Long_Name.base_name (fst (dest_Type aT)); val fs_name = PureThy.get_thm thy11 ("fs_" ^ name ^ "1"); val a = Free ("a", aT); val freshs = map (fn (f, fT) => HOLogic.mk_Trueprop @@ -2013,10 +2013,10 @@ val (reccomb_defs, thy12) = thy11 |> Sign.add_consts_i (map (fn ((name, T), T') => - (Binding.name (NameSpace.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn)) + (Binding.name (Long_Name.base_name name), rec_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_permeq.ML Sun Mar 08 17:26:14 2009 +0100 @@ -110,7 +110,7 @@ Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => (if (applicable_app f) then let - val name = NameSpace.base_name n + val name = Long_Name.base_name n val at_inst = PureThy.get_thm sg ("at_" ^ name ^ "_inst") val pt_inst = PureThy.get_thm sg ("pt_" ^ name ^ "_inst") in SOME ((at_inst RS (pt_inst RS perm_eq_app)) RS eq_reflection) end @@ -198,8 +198,8 @@ Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ pi2 $ t)) => let - val tname' = NameSpace.base_name tname - val uname' = NameSpace.base_name uname + val tname' = Long_Name.base_name tname + val uname' = Long_Name.base_name uname in if pi1 <> pi2 then (* only apply the composition rule in this case *) if T = U then diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Sun Mar 08 17:26:14 2009 +0100 @@ -207,7 +207,7 @@ val frees = ls @ x :: rs; val raw_rhs = list_abs_free (frees, list_comb (Const (rec_name, dummyT), fs @ [Free x])) - val def_name = Thm.def_name (NameSpace.base_name fname); + val def_name = Thm.def_name (Long_Name.base_name fname); val rhs = singleton (Syntax.check_terms ctxt) raw_rhs; val SOME var = get_first (fn ((b, _), mx) => if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes; @@ -286,7 +286,7 @@ fold_map (apfst (snd o snd) oo LocalTheory.define Thm.definitionK o fst) defs'; val qualify = Binding.qualify false - (space_implode "_" (map (NameSpace.base_name o #1) defs)); + (space_implode "_" (map (Long_Name.base_name o #1) defs)); val names_atts' = map (apfst qualify) names_atts; val cert = cterm_of (ProofContext.theory_of lthy'); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Mar 08 17:26:14 2009 +0100 @@ -115,7 +115,7 @@ (Var (n,ty))) => let (* FIXME: this should be an operation the library *) - val class_name = (NameSpace.map_base_name (fn s => "pt_"^s) tyatm) + val class_name = (Long_Name.map_base_name (fn s => "pt_"^s) tyatm) in if (Sign.of_sort thy (ty,[class_name])) then [(pi,typi)] diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Statespace/state_fun.ML Sun Mar 08 17:26:14 2009 +0100 @@ -336,17 +336,17 @@ [] => "" | c::cs => String.implode (Char.toUpper c::cs )) -fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (NameSpace.base_name T) - | mkName (TFree (x,_)) = mkUpper (NameSpace.base_name x) - | mkName (TVar ((x,_),_)) = mkUpper (NameSpace.base_name x); +fun mkName (Type (T,args)) = concat (map mkName args) ^ mkUpper (Long_Name.base_name T) + | mkName (TFree (x,_)) = mkUpper (Long_Name.base_name x) + | mkName (TVar ((x,_),_)) = mkUpper (Long_Name.base_name x); fun is_datatype thy n = is_some (Symtab.lookup (DatatypePackage.get_datatypes thy) n); fun mk_map "List.list" = Syntax.const "List.map" - | mk_map n = Syntax.const ("StateFun.map_" ^ NameSpace.base_name n); + | mk_map n = Syntax.const ("StateFun.map_" ^ Long_Name.base_name n); fun gen_constr_destr comp prfx thy (Type (T,[])) = - Syntax.const (deco prfx (mkUpper (NameSpace.base_name T))) + Syntax.const (deco prfx (mkUpper (Long_Name.base_name T))) | gen_constr_destr comp prfx thy (T as Type ("fun",_)) = let val (argTs,rangeT) = strip_type T; in comp @@ -360,11 +360,11 @@ then (* datatype args are recursively embedded into val *) (case argTs of [argT] => comp - ((Syntax.const (deco prfx (mkUpper (NameSpace.base_name T))))) + ((Syntax.const (deco prfx (mkUpper (Long_Name.base_name T))))) ((mk_map T $ gen_constr_destr comp prfx thy argT)) | _ => raise (TYPE ("StateFun.gen_constr_destr",[T'],[]))) else (* type args are not recursively embedded into val *) - Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (NameSpace.base_name T))) + Syntax.const (deco prfx (concat (map mkName argTs) ^ mkUpper (Long_Name.base_name T))) | gen_constr_destr thy _ _ T = raise (TYPE ("StateFun.gen_constr_destr",[T],[])); val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ a $ b) "" diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Statespace/state_space.ML Sun Mar 08 17:26:14 2009 +0100 @@ -645,7 +645,7 @@ fun update_tr ctxt [s,Free (n,_),v] = gen_update_tr false ctxt n v s; fun update_tr' ctxt [_$Free (prj,_),_$Free (inj,_),n as (_$Free (name,_)),(Const (k,_)$v),s] = - if NameSpace.base_name k = NameSpace.base_name KN then + if Long_Name.base_name k = Long_Name.base_name KN then (case get_comp (Context.Proof ctxt) name of SOME (T,_) => if inj=inject_name T andalso prj=project_name T then Syntax.const "_statespace_update" $ s $ n $ v diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/TFL/post.ML --- a/src/HOL/Tools/TFL/post.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/TFL/post.ML Sun Mar 08 17:26:14 2009 +0100 @@ -223,7 +223,7 @@ *---------------------------------------------------------------------------*) fun define_i strict thy cs ss congs wfs fid R eqs = let val {functional,pats} = Prim.mk_functional thy eqs - val (thy, def) = Prim.wfrec_definition0 thy (NameSpace.base_name fid) R functional + val (thy, def) = Prim.wfrec_definition0 thy (Long_Name.base_name fid) R functional val {induct, rules, tcs} = simplify_defn strict thy cs ss congs wfs fid pats def val rules' = @@ -248,7 +248,7 @@ fun defer_i thy congs fid eqs = let val {rules,R,theory,full_pats_TCs,SV,...} = - Prim.lazyR_def thy (NameSpace.base_name fid) congs eqs + Prim.lazyR_def thy (Long_Name.base_name fid) congs eqs val f = func_of_cond_eqn (concl (R.CONJUNCT1 rules handle U.ERR _ => rules)); val dummy = writeln "Proving induction theorem ..."; val induction = Prim.mk_induction theory diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/TFL/tfl.ML --- a/src/HOL/Tools/TFL/tfl.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/TFL/tfl.ML Sun Mar 08 17:26:14 2009 +0100 @@ -349,7 +349,7 @@ | L => mk_functional_err ("The following clauses are redundant (covered by preceding clauses): " ^ commas (map (fn i => Int.toString (i + 1)) L)) - in {functional = Abs(NameSpace.base_name fname, ftype, + in {functional = Abs(Long_Name.base_name fname, ftype, abstract_over (atom, absfree(aname,atype, case_tm))), pats = patts2} diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_abs_proofs.ML --- a/src/HOL/Tools/datatype_abs_proofs.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_abs_proofs.ML Sun Mar 08 17:26:14 2009 +0100 @@ -235,10 +235,10 @@ val (reccomb_defs, thy2) = thy1 |> Sign.add_consts_i (map (fn ((name, T), T') => - (Binding.name (NameSpace.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn)) + (Binding.name (Long_Name.base_name name), reccomb_fn_Ts @ [T] ---> T', NoSyn)) (reccomb_names ~~ recTs ~~ rec_result_Ts)) |> (PureThy.add_defs false o map Thm.no_attributes) (map (fn ((((name, comb), set), T), T') => - (Binding.name (NameSpace.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, + (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (comb, absfree ("x", T, Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T', set $ Free ("x", T) $ Free ("y", T')))))) (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) @@ -316,8 +316,8 @@ val fns = (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))); val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T'); - val decl = ((Binding.name (NameSpace.base_name name), caseT), NoSyn); - val def = (Binding.name (NameSpace.base_name name ^ "_def"), + val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn); + val def = (Binding.name (Long_Name.base_name name ^ "_def"), Logic.mk_equals (list_comb (Const (name, caseT), fns1), list_comb (reccomb, (List.concat (Library.take (i, case_dummy_fns))) @ fns2 @ (List.concat (Library.drop (i + 1, case_dummy_fns))) ))); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_aux.ML --- a/src/HOL/Tools/datatype_aux.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_aux.ML Sun Mar 08 17:26:14 2009 +0100 @@ -224,7 +224,7 @@ | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]); fun name_of_typ (Type (s, Ts)) = - let val s' = NameSpace.base_name s + let val s' = Long_Name.base_name s in space_implode "_" (List.filter (not o equal "") (map name_of_typ Ts) @ [if Syntax.is_identifier s' then s' else "x"]) end diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -174,9 +174,9 @@ fun dt_cases (descr: descr) (_, args, constrs) = let - fun the_bname i = NameSpace.base_name (#1 (the (AList.lookup (op =) descr i))); + fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i))); val bnames = map the_bname (distinct (op =) (maps dt_recs args)); - in map (fn (c, _) => space_implode "_" (NameSpace.base_name c :: bnames)) constrs end; + in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end; fun induct_cases descr = @@ -519,7 +519,7 @@ val cs = map (apsnd (map norm_constr)) raw_cs; val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o fst o strip_type; - val new_type_names = map NameSpace.base_name (the_default (map fst cs) alt_names); + val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names); fun mk_spec (i, (tyco, constr)) = (i, (tyco, map (DtTFree o fst) vs, diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_prop.ML Sun Mar 08 17:26:14 2009 +0100 @@ -47,7 +47,7 @@ let fun type_name (TFree (name, _)) = implode (tl (explode name)) | type_name (Type (name, _)) = - let val name' = NameSpace.base_name name + let val name' = Long_Name.base_name name in if Syntax.is_identifier name' then name' else "x" end; in indexify_names (map type_name Ts) end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_realizer.ML --- a/src/HOL/Tools/datatype_realizer.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_realizer.ML Sun Mar 08 17:26:14 2009 +0100 @@ -168,7 +168,7 @@ val Ts = map (typ_of_dtyp descr sorts) cargs; val frees = Name.variant_list ["P", "y"] (DatatypeProp.make_tnames Ts) ~~ Ts; val free_ts = map Free frees; - val r = Free ("r" ^ NameSpace.base_name cname, Ts ---> rT) + val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT) in (r, list_all_free (frees, Logic.mk_implies (HOLogic.mk_Trueprop (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))), HOLogic.mk_Trueprop (Free ("P", rT --> HOLogic.boolT) $ diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Sun Mar 08 17:26:14 2009 +0100 @@ -236,7 +236,7 @@ val lhs = list_comb (Const (cname, constrT), l_args); val rhs = mk_univ_inj r_args n i; val def = Logic.mk_equals (lhs, Const (abs_name, Univ_elT --> T) $ rhs); - val def_name = NameSpace.base_name cname ^ "_def"; + val def_name = Long_Name.base_name cname ^ "_def"; val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (rep_name, T --> Univ_elT) $ lhs, rhs)); val ([def_thm], thy') = @@ -343,7 +343,7 @@ val (fs, eqns, isos) = Library.foldl process_dt (([], [], []), ds); val fTs = map fastype_of fs; - val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (NameSpace.base_name iso_name ^ "_def"), + val defs = map (fn (rec_name, (T, iso_name)) => (Binding.name (Long_Name.base_name iso_name ^ "_def"), Logic.mk_equals (Const (iso_name, T --> Univ_elT), list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs)))) (rec_names ~~ isos); val (def_thms, thy') = diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/function_package/fundef_package.ML --- a/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -54,7 +54,7 @@ val simps_by_f = sort saved_simps fun add_for_f fname simps = - note_theorem ((NameSpace.qualified fname label, []), simps) #> snd + note_theorem ((Long_Name.qualify fname label, []), simps) #> snd in (saved_simps, fold2 add_for_f fnames simps_by_f lthy) @@ -66,12 +66,12 @@ cont (Thm.close_derivation proof) val fnames = map (fst o fst) fixes - val qualify = NameSpace.qualified defname + val qualify = Long_Name.qualify defname val addsmps = add_simps fnames post sort_cont val (((psimps', pinducts'), (_, [termination'])), lthy) = lthy - |> addsmps (NameSpace.qualified "partial") "psimps" + |> addsmps (Long_Name.qualify "partial") "psimps" [Attrib.internal (K Nitpick_Const_Psimp_Thms.add)] psimps ||> fold_option (snd oo addsmps I "simps" [Attrib.internal (K Nitpick_Const_Simp_Thms.add)]) trsimps ||>> note_theorem ((qualify "pinduct", @@ -131,7 +131,7 @@ val allatts = (not has_guards ? cons Code.add_default_eqn_attrib) [Attrib.internal (K Nitpick_Const_Simp_Thms.add)] - val qualify = NameSpace.qualified defname; + val qualify = Long_Name.qualify defname; in lthy |> add_simps I "simps" allatts tsimps |> snd diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/function_package/size.ML --- a/src/HOL/Tools/function_package/size.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/function_package/size.ML Sun Mar 08 17:26:14 2009 +0100 @@ -87,7 +87,7 @@ recTs1 ~~ alt_names' |> map (fn (T as Type (s, _), optname) => let - val s' = the_default (NameSpace.base_name s) optname ^ "_size"; + val s' = the_default (Long_Name.base_name s) optname ^ "_size"; val s'' = Sign.full_bname thy s' in (s'', @@ -140,7 +140,7 @@ val ((size_def_thms, size_def_thms'), thy') = thy |> Sign.add_consts_i (map (fn (s, T) => - (Binding.name (NameSpace.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) + (Binding.name (Long_Name.base_name s), param_size_fTs @ [T] ---> HOLogic.natT, NoSyn)) (size_names ~~ recTs1)) |> PureThy.add_defs false (map (Thm.no_attributes o apsnd (Logic.mk_equals o apsnd (app fs))) @@ -221,8 +221,8 @@ fun add_size_thms (new_type_names as name :: _) thy = let val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name; - val prefix = NameSpace.map_base_name (K (space_implode "_" - (the_default (map NameSpace.base_name new_type_names) alt_names))) name; + val prefix = Long_Name.map_base_name (K (space_implode "_" + (the_default (map Long_Name.base_name new_type_names) alt_names))) name; val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr in if no_size then thy diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/inductive_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -698,7 +698,7 @@ ctxt1 |> LocalTheory.note kind ((rec_qualified (Binding.name "intros"), []), intrs') ||>> fold_map (fn (name, (elim, cases)) => - LocalTheory.note kind ((Binding.name (NameSpace.qualified (NameSpace.base_name name) "cases"), + LocalTheory.note kind ((Binding.name (Long_Name.qualify (Long_Name.base_name name) "cases"), [Attrib.internal (K (RuleCases.case_names cases)), Attrib.internal (K (RuleCases.consumes 1)), Attrib.internal (K (Induct.cases_pred name)), diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 08 17:26:14 2009 +0100 @@ -68,8 +68,8 @@ val (Const (s, _), ts) = strip_comb (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of (hd intrs)))); val params = map dest_Var (Library.take (nparms, ts)); - val tname = Binding.name (space_implode "_" (NameSpace.base_name s ^ "T" :: vs)); - fun constr_of_intr intr = (Binding.name (NameSpace.base_name (name_of_thm intr)), + val tname = Binding.name (space_implode "_" (Long_Name.base_name s ^ "T" :: vs)); + fun constr_of_intr intr = (Binding.name (Long_Name.base_name (name_of_thm intr)), map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @ filter_out (equal Extraction.nullT) (map (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)), @@ -112,7 +112,7 @@ val rT = if n then Extraction.nullT else Type (space_implode "_" (s ^ "T" :: vs), map (fn a => TVar (("'" ^ a, 0), HOLogic.typeS)) vs @ Tvs); - val r = if n then Extraction.nullt else Var ((NameSpace.base_name s, 0), rT); + val r = if n then Extraction.nullt else Var ((Long_Name.base_name s, 0), rT); val S = list_comb (h, params @ xs); val rvs = relevant_vars S; val vs' = map fst rvs \\ vs; @@ -195,7 +195,7 @@ in if conclT = Extraction.nullT then list_abs_free (map dest_Free xs, HOLogic.unit) else list_abs_free (map dest_Free xs, list_comb - (Free ("r" ^ NameSpace.base_name (name_of_thm intr), + (Free ("r" ^ Long_Name.base_name (name_of_thm intr), map fastype_of (rev args) ---> conclT), rev args)) end @@ -217,7 +217,7 @@ end) (premss ~~ dummies); val frees = fold Term.add_frees fs []; val Ts = map fastype_of fs; - fun name_of_fn intr = "r" ^ NameSpace.base_name (name_of_thm intr) + fun name_of_fn intr = "r" ^ Long_Name.base_name (name_of_thm intr) in fst (fold_map (fn concl => fn names => let val T = Extraction.etype_of thy vs [] concl @@ -245,7 +245,7 @@ |-> (fn dtinfo => pair (map fst dts, SOME dtinfo)) handle DatatypeAux.Datatype_Empty name' => let - val name = NameSpace.base_name name'; + val name = Long_Name.base_name name'; val dname = Name.variant used "Dummy"; in thy @@ -273,8 +273,8 @@ fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) = let - val qualifier = NameSpace.qualifier (name_of_thm induct); - val inducts = PureThy.get_thms thy (NameSpace.qualified qualifier "inducts"); + val qualifier = Long_Name.qualifier (name_of_thm induct); + val inducts = PureThy.get_thms thy (Long_Name.qualify qualifier "inducts"); val iTs = OldTerm.term_tvars (prop_of (hd intrs)); val ar = length vs + length iTs; val params = InductivePackage.params_of raw_induct; @@ -285,18 +285,18 @@ val rss' = map (fn (((s, rs), (_, arity)), elim) => (s, (InductivePackage.infer_intro_vars elim arity rs ~~ rs))) (rss ~~ arities ~~ elims); - val (prfx, _) = split_last (NameSpace.explode (fst (hd rss))); + val (prfx, _) = split_last (Long_Name.explode (fst (hd rss))); val tnames = map (fn s => space_implode "_" (s ^ "T" :: vs)) rsets; val thy1 = thy |> Sign.root_path |> - Sign.add_path (NameSpace.implode prfx); + Sign.add_path (Long_Name.implode prfx); val (ty_eqs, rlz_eqs) = split_list (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss); val thy1' = thy1 |> Theory.copy |> - Sign.add_types (map (fn s => (Binding.name (NameSpace.base_name s), ar, NoSyn)) tnames) |> + Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |> fold (fn s => AxClass.axiomatize_arity (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |> Extraction.add_typeof_eqns_i ty_eqs; @@ -334,7 +334,7 @@ rintrs |> map (fn rintr => let val Const (s, T) = head_of (HOLogic.dest_Trueprop (Logic.strip_assums_concl rintr)); - val s' = NameSpace.base_name s; + val s' = Long_Name.base_name s; val T' = Logic.unvarifyT T; in (((s', T'), NoSyn), (Const (s, T'), Free (s', T'))) end) |> distinct (op = o pairself (#1 o #1)) @@ -352,7 +352,7 @@ {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty, coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false} rlzpreds rlzparams (map (fn (rintr, intr) => - ((Binding.name (NameSpace.base_name (name_of_thm intr)), []), + ((Binding.name (Long_Name.base_name (name_of_thm intr)), []), subst_atomic rlzpreds' (Logic.unvarify rintr))) (rintrs ~~ maps snd rss)) [] ||> Sign.absolute_path; @@ -395,12 +395,12 @@ [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac, DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]); val (thm', thy') = PureThy.store_thm (Binding.name (space_implode "_" - (NameSpace.qualified qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; + (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy; val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp))) (DatatypeAux.split_conj_thm thm'); val ([thms'], thy'') = PureThy.add_thmss [((Binding.name (space_implode "_" - (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @ + (Long_Name.qualify qualifier "inducts" :: vs' @ Ps @ ["correctness"])), thms), [])] thy'; val realizers = inducts ~~ thms' ~~ rlzs ~~ rs; in @@ -409,7 +409,7 @@ mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r)) realizers @ (case realizers of [(((ind, corr), rlz), r)] => - [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct", + [mk_realizer thy' (vs' @ Ps) (Long_Name.qualify qualifier "induct", ind, corr, rlz, r)] | _ => [])) thy'' end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/old_primrec_package.ML --- a/src/HOL/Tools/old_primrec_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/old_primrec_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -212,7 +212,7 @@ ((map snd ls) @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 ::(length ls downto 1)))) - val def_name = NameSpace.base_name fname ^ "_" ^ NameSpace.base_name tname ^ "_def"; + val def_name = Long_Name.base_name fname ^ "_" ^ Long_Name.base_name tname ^ "_def"; val def_prop = singleton (Syntax.check_terms (ProofContext.init thy)) (Logic.mk_equals (Const (fname, dummyT), rhs)); @@ -269,7 +269,7 @@ else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^ "\nare not mutually recursive"); val primrec_name = - if alt_name = "" then (space_implode "_" (map (NameSpace.base_name o #1) defs)) else alt_name; + if alt_name = "" then (space_implode "_" (map (Long_Name.base_name o #1) defs)) else alt_name; val (defs_thms', thy') = thy |> Sign.add_path primrec_name diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/primrec_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -191,7 +191,7 @@ (map snd ls @ [dummyT]) (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1)))) - val def_name = Thm.def_name (NameSpace.base_name fname); + val def_name = Thm.def_name (Long_Name.base_name fname); val rhs = singleton (Syntax.check_terms ctxt) raw_rhs; val SOME var = get_first (fn ((b, _), mx) => if Binding.name_of b = fname then SOME (b, mx) else NONE) fixes; @@ -247,7 +247,7 @@ val _ = if gen_eq_set (op =) (names1, names2) then () else primrec_error ("functions " ^ commas_quote names2 ^ "\nare not mutually recursive"); - val prefix = space_implode "_" (map (NameSpace.base_name o #1) defs); + val prefix = space_implode "_" (map (Long_Name.base_name o #1) defs); val qualify = Binding.qualify false prefix; val spec' = (map o apfst) (fn (b, attrs) => (qualify b, Code.add_default_eqn_attrib :: attrs)) spec; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/recdef_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -193,7 +193,7 @@ val _ = requires_recdef thy; val name = Sign.intern_const thy raw_name; - val bname = NameSpace.base_name name; + val bname = Long_Name.base_name name; val _ = writeln ("Defining recursive function " ^ quote name ^ " ..."); val ((eq_names, eqs), raw_eq_atts) = apfst split_list (split_list eq_srcs); @@ -233,7 +233,7 @@ fun gen_defer_recdef tfl_fn eval_thms raw_name eqs raw_congs thy = let val name = Sign.intern_const thy raw_name; - val bname = NameSpace.base_name name; + val bname = Long_Name.base_name name; val _ = requires_recdef thy; val _ = writeln ("Deferred recursive function " ^ quote name ^ " ..."); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/record_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -122,7 +122,7 @@ (* syntax *) fun prune n xs = Library.drop (n, xs); -fun prefix_base s = NameSpace.map_base_name (fn bname => s ^ bname); +fun prefix_base s = Long_Name.map_base_name (fn bname => s ^ bname); val Trueprop = HOLogic.mk_Trueprop; fun All xs t = Term.list_all_free (xs, t); @@ -433,8 +433,8 @@ fun get_extT_fields thy T = let val ((name,Ts),moreT) = dest_recT T; - val recname = let val (nm::recn::rst) = rev (NameSpace.explode name) - in NameSpace.implode (rev (nm::rst)) end; + val recname = let val (nm::recn::rst) = rev (Long_Name.explode name) + in Long_Name.implode (rev (nm::rst)) end; val midx = maxidx_of_typs (moreT::Ts); val varifyT = varifyT midx; val {records,extfields,...} = RecordsData.get thy; @@ -702,7 +702,7 @@ SOME flds => (let val (f::fs) = but_last (map fst flds); - val flds' = Sign.extern_const thy f :: map NameSpace.base_name fs; + val flds' = Sign.extern_const thy f :: map Long_Name.base_name fs; val (args',more) = split_last args; in (flds'~~args')@field_lst more end handle Library.UnequalLengths => [("",t)]) @@ -804,7 +804,7 @@ => (let val (f :: fs) = but_last flds; val flds' = apfst (Sign.extern_const thy) f - :: map (apfst NameSpace.base_name) fs; + :: map (apfst Long_Name.base_name) fs; val (args', more) = split_last args; val alphavars = map varifyT (but_last alphas); val subst = fold2 (curry (Sign.typ_match thy)) @@ -1069,7 +1069,7 @@ val {sel_upd={selectors,updates,...},extfields,...} = RecordsData.get thy; (*fun mk_abs_var x t = (x, fastype_of t);*) - fun sel_name u = NameSpace.base_name (unsuffix updateN u); + fun sel_name u = Long_Name.base_name (unsuffix updateN u); fun seed s (upd as Const (more,Type(_,[mT,_]))$ k $ r) = if has_field extfields s (domain_type' mT) then upd else seed s r @@ -1461,7 +1461,7 @@ Abs_inject=abs_inject, Abs_inverse = abs_inverse, ...} = TypedefPackage.get_info thy name; val rewrite_rule = MetaSimplifier.rewrite_rule [rec_UNIV_I, rec_True_simp]; in map rewrite_rule [abs_inject, abs_inverse, abs_induct] end; - val tname = Binding.name (NameSpace.base_name name); + val tname = Binding.name (Long_Name.base_name name); in thy |> TypecopyPackage.add_typecopy (Binding.suffix_name ext_typeN tname, alphas) repT NONE @@ -1475,7 +1475,7 @@ fun extension_definition full name fields names alphas zeta moreT more vars thy = let - val base = NameSpace.base_name; + val base = Long_Name.base_name; val fieldTs = (map snd fields); val alphas_zeta = alphas@[zeta]; val alphas_zetaTs = map (fn n => TFree (n, HOLogic.typeS)) alphas_zeta; @@ -1761,7 +1761,7 @@ val alphas = map fst args; val name = Sign.full_bname thy bname; val full = Sign.full_bname_path thy bname; - val base = NameSpace.base_name; + val base = Long_Name.base_name; val (bfields, field_syntax) = split_list (map (fn (x, T, mx) => ((x, T), mx)) raw_fields); @@ -1887,11 +1887,11 @@ fun parent_more s = if null parents then s - else mk_sel s (NameSpace.qualified (#name (List.last parents)) moreN, extT); + else mk_sel s (Long_Name.qualify (#name (List.last parents)) moreN, extT); fun parent_more_upd v s = if null parents then v$s - else let val mp = NameSpace.qualified (#name (List.last parents)) moreN; + else let val mp = Long_Name.qualify (#name (List.last parents)) moreN; in mk_upd updateN mp v s end; (*record (scheme) type abbreviation*) diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/res_atp.ML Sun Mar 08 17:26:14 2009 +0100 @@ -303,7 +303,7 @@ (*Reject theorems with names like "List.filter.filter_list_def" or "Accessible_Part.acc.defs", as these are definitions arising from packages.*) fun is_package_def a = - let val names = NameSpace.explode a + let val names = Long_Name.explode a in length names > 2 andalso not (hd names = "local") andalso @@ -378,7 +378,7 @@ (*Ignore blacklisted basenames*) fun add_multi_names ((a, ths), pairs) = - if (NameSpace.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs + if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist then pairs else add_single_names ((a, ths), pairs); fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/res_axioms.ML --- a/src/HOL/Tools/res_axioms.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/res_axioms.ML Sun Mar 08 17:26:14 2009 +0100 @@ -328,7 +328,7 @@ "cases","ext_cases"]; (*FIXME: put other record thms here, or use the "Internal" marker*) (*Keep the full complexity of the original name*) -fun flatten_name s = space_implode "_X" (NameSpace.explode s); +fun flatten_name s = space_implode "_X" (Long_Name.explode s); fun fake_name th = if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th) @@ -340,7 +340,7 @@ (*Skolemize a named theorem, with Skolem functions as additional premises.*) fun skolem_thm (s, th) = - if member (op =) multi_base_blacklist (NameSpace.base_name s) orelse bad_for_atp th then [] + if member (op =) multi_base_blacklist (Long_Name.base_name s) orelse bad_for_atp th then [] else let val ctxt0 = Variable.thm_context th @@ -428,7 +428,7 @@ val new_facts = (PureThy.facts_of thy, []) |-> Facts.fold_static (fn (name, ths) => if already_seen thy name then I else cons (name, ths)); val new_thms = (new_facts, []) |-> fold (fn (name, ths) => - if member (op =) multi_base_blacklist (NameSpace.base_name name) then I + if member (op =) multi_base_blacklist (Long_Name.base_name name) then I else fold_index (fn (i, th) => if bad_for_atp th orelse is_some (lookup_cache thy th) then I else cons (name ^ "_" ^ string_of_int (i + 1), Thm.transfer thy th)) ths); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/Tools/specification_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -24,7 +24,7 @@ val ctype = domain_type (type_of P) val cname_full = Sign.intern_const thy cname val cdefname = if thname = "" - then Thm.def_name (NameSpace.base_name cname) + then Thm.def_name (Long_Name.base_name cname) else thname val def_eq = Logic.mk_equals (Const(cname_full,ctype), HOLogic.choice_const ctype $ P) @@ -50,7 +50,7 @@ val ctype = domain_type (type_of P) val cname_full = Sign.intern_const thy cname val cdefname = if thname = "" - then Thm.def_name (NameSpace.base_name cname) + then Thm.def_name (Long_Name.base_name cname) else thname val co = Const(cname_full,ctype) val thy' = Theory.add_finals_i covld [co] thy @@ -154,7 +154,7 @@ fun mk_exist (c,prop) = let val T = type_of c - val cname = NameSpace.base_name (fst (dest_Const c)) + val cname = Long_Name.base_name (fst (dest_Const c)) val vname = if Syntax.is_identifier cname then cname else "x" diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOL/ex/Quickcheck_Generators.thy Sun Mar 08 17:26:14 2009 +0100 @@ -138,7 +138,7 @@ let val this_ty = Type (hd tycos, map TFree vs); val this_ty' = StateMonad.liftT (term_ty this_ty) @{typ seed}; - val random_name = NameSpace.base_name @{const_name random}; + val random_name = Long_Name.base_name @{const_name random}; val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); val random' = Free (random'_name, diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Sun Mar 08 17:26:14 2009 +0100 @@ -22,7 +22,7 @@ val dc_rep = %%:(dname^"_rep"); val x_name'= "x"; val x_name = idx_name eqs x_name' (n+1); - val dnam = NameSpace.base_name dname; + val dnam = Long_Name.base_name dname; val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOLCF/Tools/domain/domain_extender.ML --- a/src/HOLCF/Tools/domain/domain_extender.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_extender.ML Sun Mar 08 17:26:14 2009 +0100 @@ -103,7 +103,7 @@ (Sign.full_bname thy''' dname, map (Syntax.read_typ_global thy''') vs)) o fst) eqs'''; val cons''' = map snd eqs'''; - fun thy_type (dname,tvars) = (Binding.name (NameSpace.base_name dname), length tvars, NoSyn); + fun thy_type (dname,tvars) = (Binding.name (Long_Name.base_name dname), length tvars, NoSyn); fun thy_arity (dname,tvars) = (dname, map (snd o dest_TFree) tvars, pcpoS); val thy'' = thy''' |> Sign.add_types (map thy_type dtnvs) |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs; @@ -114,7 +114,7 @@ val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs'; fun strip ss = Library.drop (find_index_eq "'" ss +1, ss); fun typid (Type (id,_)) = - let val c = hd (Symbol.explode (NameSpace.base_name id)) + let val c = hd (Symbol.explode (Long_Name.base_name id)) in if Symbol.is_letter c then c else "t" end | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); @@ -133,7 +133,7 @@ ||>> Domain_Theorems.comp_theorems (comp_dnam, eqs); in theorems_thy - |> Sign.add_path (NameSpace.base_name comp_dnam) + |> Sign.add_path (Long_Name.base_name comp_dnam) |> (snd o (PureThy.add_thmss [((Binding.name "rews", List.concat rewss @ take_rews), [])])) |> Sign.parent_path end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOLCF/Tools/domain/domain_syntax.ML --- a/src/HOLCF/Tools/domain/domain_syntax.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_syntax.ML Sun Mar 08 17:26:14 2009 +0100 @@ -25,7 +25,7 @@ in val dtype = Type(dname,typevars); val dtype2 = foldr1 mk_ssumT (map prod cons'); - val dnam = NameSpace.base_name dname; + val dnam = Long_Name.base_name dname; val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn); val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn); val const_when = (dnam^"_when", List.foldr (op ->>) (dtype ->> freetvar "t") (map when_type cons'), NoSyn); diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sun Mar 08 17:26:14 2009 +0100 @@ -606,7 +606,7 @@ in thy - |> Sign.add_path (NameSpace.base_name dname) + |> Sign.add_path (Long_Name.base_name dname) |> (snd o (PureThy.add_thmss (map (Thm.no_attributes o apfst Binding.name) [ ("iso_rews" , iso_rews ), ("exhaust" , [exhaust] ), diff -r 9b8d9b6ef803 -r 577edc39b501 src/HOLCF/Tools/fixrec_package.ML --- a/src/HOLCF/Tools/fixrec_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/HOLCF/Tools/fixrec_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -181,7 +181,7 @@ val fixpoint = mk_fix (lambda_ctuple lhss (mk_ctuple rhss)); fun one_def (l as Free(n,_)) r = - let val b = NameSpace.base_name n + let val b = Long_Name.base_name n in ((Binding.name (b^"_def"), []), r) end | one_def _ _ = fixrec_err "fixdefs: lhs not of correct form"; fun defs [] _ = [] @@ -230,7 +230,7 @@ fun taken_names (t : term) : bstring list = let - fun taken (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs + fun taken (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs | taken (Free(a,_) , bs) = insert (op =) a bs | taken (f $ u , bs) = taken (f, taken (u, bs)) | taken (Abs(a,_,t), bs) = taken (t, insert (op =) a bs) diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/class_target.ML --- a/src/Pure/Isar/class_target.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/class_target.ML Sun Mar 08 17:26:14 2009 +0100 @@ -300,7 +300,7 @@ map (fn (c, (_, (ty, t))) => (t, Const (c, ty))) o these_operations thy; fun redeclare_const thy c = - let val b = NameSpace.base_name c + let val b = Long_Name.base_name c in Sign.intern_const thy b = c ? Variable.declare_const (b, c) end; fun synchronize_class_syntax sort base_sort ctxt = @@ -358,7 +358,7 @@ (* class target *) -val class_prefix = Logic.const_of_class o NameSpace.base_name; +val class_prefix = Logic.const_of_class o Long_Name.base_name; fun declare class pos ((c, mx), dict) thy = let @@ -475,7 +475,7 @@ fun type_name "*" = "prod" | type_name "+" = "sum" - | type_name s = sanatize_name (NameSpace.base_name s); + | type_name s = sanatize_name (Long_Name.base_name s); fun resort_terms pp algebra consts constraints ts = let diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/element.ML Sun Mar 08 17:26:14 2009 +0100 @@ -202,7 +202,7 @@ let val head = if Thm.has_name_hint th then Pretty.block [Pretty.command kind, - Pretty.brk 1, Pretty.str (NameSpace.base_name (Thm.get_name_hint th) ^ ":")] + Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")] else Pretty.command kind in Pretty.block (Pretty.fbreaks (head :: prts)) end; @@ -522,7 +522,7 @@ in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end; fun check_name name = - if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name) + if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name) else name; fun prep_facts prep_name get intern ctxt = diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/proof_context.ML Sun Mar 08 17:26:14 2009 +0100 @@ -590,7 +590,7 @@ let val _ = no_skolem false x; val sko = lookup_skolem ctxt x; - val is_const = can (read_const_proper ctxt) x orelse NameSpace.is_qualified x; + val is_const = can (read_const_proper ctxt) x orelse Long_Name.is_qualified x; val is_declared = is_some (def_type (x, ~1)); in if Variable.is_const ctxt x then NONE diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/proof_display.ML Sun Mar 08 17:26:14 2009 +0100 @@ -75,7 +75,7 @@ fun pretty_fact_name (kind, "") = Pretty.str kind | pretty_fact_name (kind, name) = Pretty.block [Pretty.str kind, Pretty.brk 1, - Pretty.str (NameSpace.base_name name), Pretty.str ":"]; + Pretty.str (Long_Name.base_name name), Pretty.str ":"]; fun pretty_facts ctxt = flat o (separate [Pretty.fbrk, Pretty.str "and "]) o diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/rule_cases.ML Sun Mar 08 17:26:14 2009 +0100 @@ -105,7 +105,7 @@ if not nested then abs_fixes t else abs fixes1 (app (map (Term.dummy_pattern o #2) fixes2) (abs fixes2 t)); - val (assumes1, assumes2) = extract_assumes (NameSpace.qualified name) case_outline prop + val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop |> pairself (map (apsnd (maps Logic.dest_conjunctions))); val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Isar/theory_target.ML --- a/src/Pure/Isar/theory_target.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Isar/theory_target.ML Sun Mar 08 17:26:14 2009 +0100 @@ -329,7 +329,7 @@ fun init_lthy (ta as Target {target, instantiation, overloading, ...}) = Data.put ta #> - LocalTheory.init (NameSpace.base_name target) + LocalTheory.init (Long_Name.base_name target) {pretty = pretty ta, abbrev = abbrev ta, define = define ta, diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/ML/ml_antiquote.ML Sun Mar 08 17:26:14 2009 +0100 @@ -110,7 +110,7 @@ fun type_ syn = (Args.context -- Scan.lift Args.name_source >> (fn (ctxt, c) => #1 (Term.dest_Type (ProofContext.read_tyname ctxt c)) - |> syn ? NameSpace.base_name + |> syn ? Long_Name.base_name |> ML_Syntax.print_string)); val _ = inline "type_name" (type_ false); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Sun Mar 08 17:26:14 2009 +0100 @@ -119,7 +119,7 @@ val chtype = change_type o SOME; -fun extr_name s vs = NameSpace.append "extr" (space_implode "_" (s :: vs)); +fun extr_name s vs = Long_Name.append "extr" (space_implode "_" (s :: vs)); fun corr_name s vs = extr_name s vs ^ "_correctness"; fun msg d s = priority (Symbol.spaces d ^ s); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sun Mar 08 17:26:14 2009 +0100 @@ -97,16 +97,16 @@ fun prf_of [] (Bound i) = PBound i | prf_of Ts (Const (s, Type ("proof", _))) = change_type (if ty then SOME Ts else NONE) - (case NameSpace.explode s of + (case Long_Name.explode s of "axm" :: xs => let - val name = NameSpace.implode xs; + val name = Long_Name.implode xs; val prop = (case AList.lookup (op =) axms name of SOME prop => prop | NONE => error ("Unknown axiom " ^ quote name)) in PAxm (name, prop, NONE) end | "thm" :: xs => - let val name = NameSpace.implode xs; + let val name = Long_Name.implode xs; in (case AList.lookup (op =) thms name of SOME thm => fst (strip_combt (Thm.proof_of thm)) | NONE => error ("Unknown theorem " ^ quote name)) @@ -147,12 +147,12 @@ [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T); fun term_of _ (PThm (_, ((name, _, NONE), _))) = - Const (NameSpace.append "thm" name, proofT) + Const (Long_Name.append "thm" name, proofT) | term_of _ (PThm (_, ((name, _, SOME Ts), _))) = - mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT)) - | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT) + mk_tyapp Ts (Const (Long_Name.append "thm" name, proofT)) + | term_of _ (PAxm (name, _, NONE)) = Const (Long_Name.append "axm" name, proofT) | term_of _ (PAxm (name, _, SOME Ts)) = - mk_tyapp Ts (Const (NameSpace.append "axm" name, proofT)) + mk_tyapp Ts (Const (Long_Name.append "axm" name, proofT)) | term_of _ (PBound i) = Bound i | term_of Ts (Abst (s, opT, prf)) = let val T = the_default dummyT opT @@ -183,7 +183,7 @@ val thy' = thy |> add_proof_syntax |> add_proof_atom_consts - (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names); + (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names); in (cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of) end; @@ -195,7 +195,7 @@ val ctxt = thy |> add_proof_syntax |> add_proof_atom_consts - (map (NameSpace.append "axm") axm_names @ map (NameSpace.append "thm") thm_names) + (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names) |> ProofContext.init |> ProofContext.allow_dummies |> ProofContext.set_mode ProofContext.mode_schematic; @@ -219,7 +219,7 @@ in add_proof_syntax #> add_proof_atom_consts - (map (NameSpace.append "thm") thm_names @ map (NameSpace.append "axm") axm_names) + (map (Long_Name.append "thm") thm_names @ map (Long_Name.append "axm") axm_names) end; fun proof_of full thm = diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sun Mar 08 17:26:14 2009 +0100 @@ -543,8 +543,8 @@ fun setids t = issue_pgip (Setids {idtables = [t]}) (* fake one-level nested "subtheories" by picking apart names. *) - val immed_thms_of_thy = filter_out NameSpace.is_qualified o thms_of_thy - fun thy_prefix s = case space_explode NameSpace.separator s of + val immed_thms_of_thy = filter_out Long_Name.is_qualified o thms_of_thy + fun thy_prefix s = case Long_Name.explode s of x::_::_ => SOME x (* String.find? *) | _ => NONE fun subthys_of_thy s = @@ -553,7 +553,7 @@ fun subthms_of_thy thy = (case thy_prefix thy of NONE => immed_thms_of_thy thy - | SOME prf => filter (String.isPrefix (unprefix (prf ^ NameSpace.separator) thy)) + | SOME prf => filter (String.isPrefix (unprefix (prf ^ Long_Name.separator) thy)) (thms_of_thy prf)) in case (thyname,objtype) of @@ -642,7 +642,7 @@ val topthy = Toplevel.theory_of o Isar.state fun splitthy id = - let val comps = NameSpace.explode id + let val comps = Long_Name.explode id in case comps of (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest) | [plainid] => (topthy(),plainid) diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Syntax/syntax.ML Sun Mar 08 17:26:14 2009 +0100 @@ -301,7 +301,7 @@ lexicon = if changed then fold Scan.extend_lexicon (SynExt.delims_of xprods) lexicon else lexicon, gram = if changed then Parser.extend_gram gram xprods else gram, - consts = Library.merge (op =) (consts1, filter_out NameSpace.is_qualified consts2), + consts = Library.merge (op =) (consts1, filter_out Long_Name.is_qualified consts2), prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)), parse_ast_trtab = update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab, @@ -607,7 +607,7 @@ fun constify (ast as Ast.Constant _) = ast | constify (ast as Ast.Variable x) = - if member (op =) consts x orelse NameSpace.is_qualified x then Ast.Constant x + if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x else ast | constify (Ast.Appl asts) = Ast.Appl (map constify asts); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Syntax/type_ext.ML Sun Mar 08 17:26:14 2009 +0100 @@ -129,7 +129,7 @@ (case (map_free a, map_const a) of (SOME x, _) => Free (x, map_type T) | (_, (true, c)) => Const (c, map_type T) - | (_, (false, c)) => (if NameSpace.is_qualified c then Const else Free) (c, map_type T)) + | (_, (false, c)) => (if Long_Name.is_qualified c then Const else Free) (c, map_type T)) | decode (Var (xi, T)) = Var (xi, map_type T) | decode (t as Bound _) = t; in decode tm end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Thy/thm_deps.ML Sun Mar 08 17:26:14 2009 +0100 @@ -20,7 +20,7 @@ fun add_dep ("", _, _) = I | add_dep (name, _, PBody {thms = thms', ...}) = let - val prefix = #1 (Library.split_last (NameSpace.explode name)); + val prefix = #1 (Library.split_last (Long_Name.explode name)); val session = (case prefix of a :: _ => @@ -33,7 +33,7 @@ | _ => ["global"]); val parents = filter_out (fn s => s = "") (map (#1 o #2) thms'); val entry = - {name = NameSpace.base_name name, + {name = Long_Name.base_name name, ID = name, dir = space_implode "/" (session @ prefix), unfold = false, diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/Tools/find_theorems.ML Sun Mar 08 17:26:14 2009 +0100 @@ -279,7 +279,7 @@ val index_ord = option_ord (K EQUAL); val hidden_ord = bool_ord o pairself NameSpace.is_hidden; -val qual_ord = int_ord o pairself (length o NameSpace.explode); +val qual_ord = int_ord o pairself (length o Long_Name.explode); val txt_ord = int_ord o pairself size; fun nicer_name (x, i) (y, j) = diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/axclass.ML Sun Mar 08 17:26:14 2009 +0100 @@ -158,7 +158,7 @@ (* maintain instances *) -fun instance_name (a, c) = NameSpace.base_name c ^ "_" ^ NameSpace.base_name a; +fun instance_name (a, c) = Long_Name.base_name c ^ "_" ^ Long_Name.base_name a; val get_instances = #1 o #2 o AxClassData.get; val map_instances = AxClassData.map o apsnd o apfst; @@ -366,7 +366,7 @@ | NONE => error ("Illegal type for instantiation of class parameter: " ^ quote (c ^ " :: " ^ Syntax.string_of_typ_global thy T)); val name_inst = instance_name (tyco, class) ^ "_inst"; - val c' = NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco; + val c' = Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco; val T' = Type.strip_sorts T; in thy @@ -390,7 +390,7 @@ val SOME tyco = inst_tyco_of thy (c, T); val (c', eq) = get_inst_param thy (c, tyco); val prop = Logic.mk_equals (Const (c', T), t); - val name' = Thm.def_name_optional (NameSpace.base_name c ^ "_" ^ NameSpace.base_name tyco) name; + val name' = Thm.def_name_optional (Long_Name.base_name c ^ "_" ^ Long_Name.base_name tyco) name; in thy |> Thm.add_def false false (Binding.name name', prop) diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/codegen.ML Sun Mar 08 17:26:14 2009 +0100 @@ -378,7 +378,7 @@ | (true, "isup") => "" :: check_str zs | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs) | (ys, zs) => implode ys :: check_str zs); - val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s)) + val s' = space_implode "_" (maps (check_str o Symbol.explode) (Long_Name.explode s)) in if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' end; @@ -388,8 +388,8 @@ fun find_name [] = sys_error "mk_long_id" | find_name (ys :: yss) = let - val s' = NameSpace.implode ys - val s'' = NameSpace.append module s' + val s' = Long_Name.implode ys + val s'' = Long_Name.append module s' in case Symtab.lookup used s'' of NONE => ((module, s'), (Symtab.update_new (s, (module, s')) tab, @@ -397,7 +397,7 @@ | SOME _ => find_name yss end in case Symtab.lookup tab s of - NONE => find_name (Library.suffixes1 (NameSpace.explode s)) + NONE => find_name (Library.suffixes1 (Long_Name.explode s)) | SOME name => (name, p) end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/consts.ML --- a/src/Pure/consts.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/consts.ML Sun Mar 08 17:26:14 2009 +0100 @@ -117,7 +117,7 @@ fun syntax consts (c, mx) = let val ({T, authentic, ...}, _) = the_const consts c handle TYPE (msg, _, _) => error msg; - val c' = if authentic then Syntax.constN ^ c else NameSpace.base_name c; + val c' = if authentic then Syntax.constN ^ c else Long_Name.base_name c; in (c', T, mx) end; fun syntax_name consts c = #1 (syntax consts (c, NoSyn)); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/logic.ML --- a/src/Pure/logic.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/logic.ML Sun Mar 08 17:26:14 2009 +0100 @@ -230,7 +230,7 @@ (* class relations *) fun name_classrel (c1, c2) = - NameSpace.base_name c1 ^ "_" ^ NameSpace.base_name c2; + Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); @@ -243,8 +243,8 @@ (* type arities *) fun name_arities (t, _, S) = - let val b = NameSpace.base_name t - in S |> map (fn c => NameSpace.base_name c ^ "_" ^ b) end; + let val b = Long_Name.base_name t + in S |> map (fn c => Long_Name.base_name c ^ "_" ^ b) end; fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/old_term.ML --- a/src/Pure/old_term.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/old_term.ML Sun Mar 08 17:26:14 2009 +0100 @@ -39,7 +39,7 @@ (*Accumulates the names in the term, suppressing duplicates. Includes Frees and Consts. For choosing unambiguous bound var names.*) -fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base_name a) bs +fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs | add_term_names (Free(a,_), bs) = insert (op =) a bs | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/primitive_defs.ML Sun Mar 08 17:26:14 2009 +0100 @@ -81,7 +81,7 @@ fun mk_defpair (lhs, rhs) = (case Term.head_of lhs of Const (name, _) => - (NameSpace.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) + (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs)) | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); end; diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/sign.ML --- a/src/Pure/sign.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/sign.ML Sun Mar 08 17:26:14 2009 +0100 @@ -355,7 +355,7 @@ fun check_vars (t $ u) = (check_vars t; check_vars u) | check_vars (Abs (_, _, t)) = check_vars t | check_vars (Free (x, _)) = - if NameSpace.is_qualified x then err ("Malformed variable: " ^ quote x) else () + if Long_Name.is_qualified x then err ("Malformed variable: " ^ quote x) else () | check_vars (Var (xi as (_, i), _)) = if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else () | check_vars _ = (); diff -r 9b8d9b6ef803 -r 577edc39b501 src/Pure/term.ML --- a/src/Pure/term.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Pure/term.ML Sun Mar 08 17:26:14 2009 +0100 @@ -490,7 +490,7 @@ fun declare_term_names tm = fold_aterms - (fn Const (a, _) => Name.declare (NameSpace.base_name a) + (fn Const (a, _) => Name.declare (Long_Name.base_name a) | Free (a, _) => Name.declare a | _ => I) tm #> fold_types declare_typ_names tm; @@ -721,7 +721,7 @@ fun lambda v t = let val x = (case v of - Const (x, _) => NameSpace.base_name x + Const (x, _) => Long_Name.base_name x | Free (x, _) => x | Var ((x, _), _) => x | _ => Name.uu) diff -r 9b8d9b6ef803 -r 577edc39b501 src/Tools/code/code_haskell.ML --- a/src/Tools/code/code_haskell.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Tools/code/code_haskell.ML Sun Mar 08 17:26:14 2009 +0100 @@ -34,7 +34,7 @@ fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const init_syms deresolve is_cons contr_classparam_typs deriving_show = let - val deresolve_base = NameSpace.base_name o deresolve; + val deresolve_base = Long_Name.base_name o deresolve; fun class_name class = case syntax_class class of NONE => deresolve class | SOME class => class; @@ -143,7 +143,7 @@ @ str "=" :: str "error" @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string - o NameSpace.base_name o NameSpace.qualifier) name + o Long_Name.base_name o Long_Name.qualifier) name ) ] end @@ -155,7 +155,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = init_syms |> Code_Name.intro_vars consts @@ -255,7 +255,7 @@ let val (c_inst_name, (_, tys)) = c_inst; val const = if (is_some o syntax_const) c_inst_name - then NONE else (SOME o NameSpace.base_name o deresolve) c_inst_name; + then NONE else (SOME o Long_Name.base_name o deresolve) c_inst_name; val proto_rhs = Code_Thingol.eta_expand k (c_inst, []); val (vs, rhs) = unfold_abs_pure proto_rhs; val vars = init_syms @@ -313,11 +313,11 @@ | Code_Thingol.Classinst _ => pair base; fun add_stmt' base' = case stmt of Code_Thingol.Datatypecons _ => - cons (name, (NameSpace.append module_name' base', NONE)) + cons (name, (Long_Name.append module_name' base', NONE)) | Code_Thingol.Classrel _ => I | Code_Thingol.Classparam _ => - cons (name, (NameSpace.append module_name' base', NONE)) - | _ => cons (name, (NameSpace.append module_name' base', SOME stmt)); + cons (name, (Long_Name.append module_name' base', NONE)) + | _ => cons (name, (Long_Name.append module_name' base', SOME stmt)); in Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names)))) (apfst (fold (insert (op = : string * string -> bool)) deps)) @@ -360,7 +360,7 @@ val reserved_names = Code_Name.make_vars reserved_names; fun pr_stmt qualified = pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const reserved_names - (if qualified then deresolver else NameSpace.base_name o deresolver) + (if qualified then deresolver else Long_Name.base_name o deresolver) is_cons contr_classparam_typs (if string_classes then deriving_show else K false); fun pr_module name content = @@ -379,10 +379,10 @@ |> map_filter (try deresolver); val qualified = is_none module_name andalso map deresolver stmt_names @ deps' - |> map NameSpace.base_name + |> map Long_Name.base_name |> has_duplicates (op =); val imports = deps' - |> map NameSpace.qualifier + |> map Long_Name.qualifier |> distinct (op =); fun pr_import_include (name, _) = str ("import qualified " ^ name ^ ";"); val pr_import_module = str o (if qualified @@ -413,7 +413,7 @@ val filename = case modlname of "" => Path.explode "Main.hs" | _ => (Path.ext "hs" o Path.explode o implode o separate "/" - o NameSpace.explode) modlname; + o Long_Name.explode) modlname; val pathname = Path.append destination filename; val _ = File.mkdir (Path.dir pathname); in File.write pathname diff -r 9b8d9b6ef803 -r 577edc39b501 src/Tools/code/code_ml.ML --- a/src/Tools/code/code_ml.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Tools/code/code_ml.ML Sun Mar 08 17:26:14 2009 +0100 @@ -46,8 +46,8 @@ fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons = let val pr_label_classrel = translate_string (fn "." => "__" | c => c) - o NameSpace.qualifier; - val pr_label_classparam = NameSpace.base_name o NameSpace.qualifier; + o Long_Name.qualifier; + val pr_label_classparam = Long_Name.base_name o Long_Name.qualifier; fun pr_dicts fxy ds = let fun pr_dictvar (v, (_, 1)) = Code_Name.first_upper v ^ "_" @@ -163,7 +163,7 @@ fun pr_stmt (MLExc (name, n)) = let val exc_str = - (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name; + (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; in concat ( str (if n = 0 then "val" else "fun") @@ -179,7 +179,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names |> Code_Name.intro_vars consts; @@ -204,7 +204,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -473,7 +473,7 @@ fun pr_stmt (MLExc (name, n)) = let val exc_str = - (ML_Syntax.print_string o NameSpace.base_name o NameSpace.qualifier) name; + (ML_Syntax.print_string o Long_Name.base_name o Long_Name.qualifier) name; in concat ( str "let" @@ -488,7 +488,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) (Code_Thingol.fold_constnames (insert (op =)) t []); val vars = reserved_names |> Code_Name.intro_vars consts; @@ -508,7 +508,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -524,7 +524,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []); val vars = reserved_names |> Code_Name.intro_vars consts @@ -552,7 +552,7 @@ let val consts = map_filter (fn c => if (is_some o syntax_const) c - then NONE else (SOME o NameSpace.base_name o deresolve) c) + then NONE else (SOME o Long_Name.base_name o deresolve) c) ((fold o Code_Thingol.fold_constnames) (insert (op =)) (map (snd o fst) eqs) []); val vars = reserved_names @@ -860,7 +860,7 @@ ^ commas (map labelled_name names) ^ "\n" ^ commas module_names); - val module_name_path = NameSpace.explode module_name; + val module_name_path = Long_Name.explode module_name; fun add_dep name name' = let val module_name' = (mk_name_module o fst o Code_Name.dest_name) name'; @@ -868,7 +868,7 @@ map_node module_name_path (Graph.add_edge (name, name')) else let val (common, (diff1 :: _, diff2 :: _)) = chop_prefix (op =) - (module_name_path, NameSpace.explode module_name'); + (module_name_path, Long_Name.explode module_name'); in map_node common (fn node => Graph.add_edge_acyclic (diff1, diff2) node @@ -892,7 +892,7 @@ fun deresolver prefix name = let val module_name = (fst o Code_Name.dest_name) name; - val module_name' = (NameSpace.explode o mk_name_module) module_name; + val module_name' = (Long_Name.explode o mk_name_module) module_name; val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name'); val stmt_name = nodes @@ -901,7 +901,7 @@ |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name | Dummy stmt_name => stmt_name); in - NameSpace.implode (remainder @ [stmt_name]) + Long_Name.implode (remainder @ [stmt_name]) end handle Graph.UNDEF _ => error ("Unknown statement name: " ^ labelled_name name); in (deresolver, nodes) end; @@ -1011,7 +1011,7 @@ let val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt; val (raw_ml_code, consts_map) = Lazy.force acc_code; - val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name) + val const'' = Long_Name.append (Long_Name.append struct_name struct_code_name) ((the o AList.lookup (op =) consts_map) const); val ml_code = if is_first then "\nstructure " ^ struct_code_name ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n" diff -r 9b8d9b6ef803 -r 577edc39b501 src/Tools/code/code_name.ML --- a/src/Tools/code/code_name.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Tools/code/code_name.ML Sun Mar 08 17:26:14 2009 +0100 @@ -39,7 +39,7 @@ val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode; val dest_name = - apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode; + apfst Long_Name.implode o split_last o fst o split_last o Long_Name.explode; (** purification **) @@ -80,7 +80,7 @@ #> Symbol.scanner "Malformed name" (Scan.repeat ($$ "_" |-- $$ "_" >> (fn _ => ".") || Scan.one Symbol.is_regular)) #> implode - #> NameSpace.explode + #> Long_Name.explode #> map (purify_name true false); (*FIMXE non-canonical function treating non-canonical names*) @@ -101,11 +101,11 @@ fun check_modulename mn = let - val mns = NameSpace.explode mn; + val mns = Long_Name.explode mn; val mns' = map (purify_name true false) mns; in if mns' = mns then mn else error ("Invalid module name: " ^ quote mn ^ "\n" - ^ "perhaps try " ^ quote (NameSpace.implode mns')) + ^ "perhaps try " ^ quote (Long_Name.implode mns')) end; @@ -155,11 +155,11 @@ fun mk_alias name = case module_alias name of SOME name' => name' | NONE => name - |> NameSpace.explode + |> Long_Name.explode |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names)) - |> NameSpace.implode; + |> Long_Name.implode; fun mk_prefix name = case module_prefix - of SOME module_prefix => NameSpace.append module_prefix name + of SOME module_prefix => Long_Name.append module_prefix name | NONE => name; val tab = Symtab.empty diff -r 9b8d9b6ef803 -r 577edc39b501 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/Tools/code/code_thingol.ML Sun Mar 08 17:26:14 2009 +0100 @@ -243,18 +243,18 @@ let val prefix = get_thyname thy name; val base = (Code_Name.purify_base true o get_basename) name; - in NameSpace.append prefix base end; + in Long_Name.append prefix base end; in -fun namify_class thy = namify thy NameSpace.base_name thyname_of_class; +fun namify_class thy = namify thy Long_Name.base_name thyname_of_class; fun namify_classrel thy = namify thy (fn (class1, class2) => - NameSpace.base_name class2 ^ "_" ^ NameSpace.base_name class1) (fn thy => thyname_of_class thy o fst); + Long_Name.base_name class2 ^ "_" ^ Long_Name.base_name class1) (fn thy => thyname_of_class thy o fst); (*order fits nicely with composed projections*) fun namify_tyco thy "fun" = "Pure.fun" - | namify_tyco thy tyco = namify thy NameSpace.base_name thyname_of_tyco tyco; + | namify_tyco thy tyco = namify thy Long_Name.base_name thyname_of_tyco tyco; fun namify_instance thy = namify thy (fn (class, tyco) => - NameSpace.base_name class ^ "_" ^ NameSpace.base_name tyco) thyname_of_instance; -fun namify_const thy = namify thy NameSpace.base_name thyname_of_const; + Long_Name.base_name class ^ "_" ^ Long_Name.base_name tyco) thyname_of_instance; +fun namify_const thy = namify thy Long_Name.base_name thyname_of_const; end; (* local *) @@ -327,7 +327,7 @@ val suffix_const = "const"; fun add_suffix nsp NONE = NONE - | add_suffix nsp (SOME name) = SOME (NameSpace.append name nsp); + | add_suffix nsp (SOME name) = SOME (Long_Name.append name nsp); in diff -r 9b8d9b6ef803 -r 577edc39b501 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/ZF/Tools/datatype_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -74,7 +74,7 @@ Syntax.string_of_term_global thy t); val rec_names = map (#1 o dest_Const) rec_hds - val rec_base_names = map NameSpace.base_name rec_names + val rec_base_names = map Long_Name.base_name rec_names val big_rec_base_name = space_implode "_" rec_base_names val thy_path = thy |> Sign.add_path big_rec_base_name diff -r 9b8d9b6ef803 -r 577edc39b501 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Sun Mar 08 17:26:14 2009 +0100 @@ -157,7 +157,7 @@ in thy - |> Sign.add_path (NameSpace.base_name big_rec_name) + |> Sign.add_path (Long_Name.base_name big_rec_name) |> PureThy.add_thmss [((Binding.name "simps", simps), [Simplifier.simp_add])] |> snd |> DatatypesData.put (Symtab.update (big_rec_name, dt_info) (DatatypesData.get thy)) |> ConstructorsData.put (fold_rev Symtab.update con_pairs (ConstructorsData.get thy)) diff -r 9b8d9b6ef803 -r 577edc39b501 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/ZF/Tools/inductive_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -80,7 +80,7 @@ val rec_names = map (#1 o dest_Const) rec_hds and (Const(_,recT),rec_params) = strip_comb (hd rec_tms); - val rec_base_names = map NameSpace.base_name rec_names; + val rec_base_names = map Long_Name.base_name rec_names; val dummy = assert_all Syntax.is_identifier rec_base_names (fn a => "Base name of recursive set not an identifier: " ^ a); @@ -377,7 +377,7 @@ mutual recursion to invariably be a disjoint sum.*) fun mk_predpair rec_tm = let val rec_name = (#1 o dest_Const o head_of) rec_tm - val pfree = Free(pred_name ^ "_" ^ NameSpace.base_name rec_name, + val pfree = Free(pred_name ^ "_" ^ Long_Name.base_name rec_name, elem_factors ---> FOLogic.oT) val qconcl = List.foldr FOLogic.mk_all diff -r 9b8d9b6ef803 -r 577edc39b501 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Sun Mar 08 17:19:15 2009 +0100 +++ b/src/ZF/Tools/primrec_package.ML Sun Mar 08 17:26:14 2009 +0100 @@ -139,7 +139,7 @@ (** make definition **) (*the recursive argument*) - val rec_arg = Free (Name.variant (map #1 (ls@rs)) (NameSpace.base_name big_rec_name), + val rec_arg = Free (Name.variant (map #1 (ls@rs)) (Long_Name.base_name big_rec_name), Ind_Syntax.iT) val def_tm = Logic.mk_equals @@ -153,7 +153,7 @@ writeln ("primrec def:\n" ^ Syntax.string_of_term_global thy def_tm) else(); - (NameSpace.base_name fname ^ "_" ^ NameSpace.base_name big_rec_name ^ "_def", + (Long_Name.base_name fname ^ "_" ^ Long_Name.base_name big_rec_name ^ "_def", def_tm) end; @@ -168,7 +168,7 @@ val def = process_fun thy (fname, ftype, ls, rs, con_info, eqns); val ([def_thm], thy1) = thy - |> Sign.add_path (NameSpace.base_name fname) + |> Sign.add_path (Long_Name.base_name fname) |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name def)]; val rewrites = def_thm :: map mk_meta_eq (#rec_rewrites con_info)