--- a/src/Doc/Implementation/Prelim.thy Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Doc/Implementation/Prelim.thy Tue Mar 31 00:21:07 2015 +0200
@@ -917,7 +917,7 @@
@{index_ML Binding.name: "string -> binding"} \\
@{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
@{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
- @{index_ML Binding.conceal: "binding -> binding"} \\
+ @{index_ML Binding.concealed: "binding -> binding"} \\
@{index_ML Binding.print: "binding -> string"} \\
\end{mldecls}
\begin{mldecls}
@@ -961,7 +961,7 @@
typically used in the infrastructure for modular specifications,
notably ``local theory targets'' (see also \chref{ch:local-theory}).
- \item @{ML Binding.conceal}~@{text "binding"} indicates that the
+ \item @{ML Binding.concealed}~@{text "binding"} indicates that the
binding shall refer to an entity that serves foundational purposes
only. This flag helps to mark implementation details of
specification mechanism etc. Other tools should not depend on the
--- a/src/HOL/Nominal/nominal_datatype.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Tue Mar 31 00:21:07 2015 +0200
@@ -529,7 +529,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
thy3
- |> Sign.map_naming Name_Space.conceal
+ |> Sign.map_naming Name_Space.concealed
|> Inductive.add_inductive_global
{quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true}
@@ -1505,7 +1505,7 @@
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
thy10
- |> Sign.map_naming Name_Space.conceal
+ |> Sign.map_naming Name_Space.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = false, no_ind = false, skip_mono = true}
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Tue Mar 31 00:21:07 2015 +0200
@@ -1006,10 +1006,7 @@
val def_thm =
case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
rtac def_thm 1 THEN rest (tl skel) memo
end
@@ -1018,10 +1015,7 @@
val ax_thm =
case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
rtac ax_thm 1 THEN rest (tl skel) memo
end
@@ -1184,10 +1178,7 @@
fun def_thm thy =
case AList.lookup (op =) (#defs pannot) n of
NONE => error ("Did not find definition: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
(hd skel,
Thm.prop_of (def_thm thy)
@@ -1200,10 +1191,7 @@
val ax_thm =
case AList.lookup (op =) (#axs pannot) n of
NONE => error ("Did not find axiom: " ^ n)
- | SOME binding =>
- Binding.dest binding
- |> #3
- |> Global_Theory.get_thm thy
+ | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding)
in
(hd skel,
Thm.prop_of ax_thm
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Mar 31 00:21:07 2015 +0200
@@ -2057,9 +2057,9 @@
fun values () =
case role of
TPTP_Syntax.Role_Definition =>
- map (apsnd Binding.dest) (#defs pannot)
+ map (apsnd Binding.name_of) (#defs pannot)
| TPTP_Syntax.Role_Axiom =>
- map (apsnd Binding.dest) (#axs pannot)
+ map (apsnd Binding.name_of) (#axs pannot)
| _ => raise UNSUPPORTED_ROLE
in
if is_none (source_inf_opt node) then []
@@ -2075,7 +2075,7 @@
use the ones in the proof annotation.*)
(fn x =>
if role = TPTP_Syntax.Role_Definition then
- let fun values () = map (apsnd Binding.dest) (#defs pannot)
+ let fun values () = map (apsnd Binding.name_of) (#defs pannot)
in
map snd (values ())
end
@@ -2086,7 +2086,7 @@
val roled_dependencies =
roled_dependencies_names
- #> map (#3 #> Global_Theory.get_thm thy)
+ #> map (Global_Theory.get_thm thy)
in
val depends_on_defs = roled_dependencies TPTP_Syntax.Role_Definition
val depends_on_axs = roled_dependencies TPTP_Syntax.Role_Axiom
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Tue Mar 31 00:21:07 2015 +0200
@@ -899,7 +899,7 @@
val bnf_b = qualify b;
val def_qualify =
- Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
+ Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
val map_b = def_qualify (mk_prefix_binding mapN);
val rel_b = def_qualify (mk_prefix_binding relN);
--- a/src/HOL/Tools/BNF/bnf_def.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Tue Mar 31 00:21:07 2015 +0200
@@ -689,7 +689,7 @@
val facts = facts_of_bnf bnf;
val wits = wits_of_bnf bnf;
val qualify =
- let val (_, qs, _) = Binding.dest bnf_b;
+ let val qs = Binding.path_of bnf_b;
in fold_rev (fn (s, mand) => Binding.qualify mand s) qs #> qualify0 end;
fun note_if_note_all (noted0, lthy0) =
@@ -765,7 +765,7 @@
let
val live = length set_rhss;
- val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
+ val def_qualify = Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Mar 31 00:21:07 2015 +0200
@@ -1218,7 +1218,7 @@
val thy = Proof_Context.theory_of lthy0;
val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
+ #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
val ((cst, (_, def)), (lthy', lthy)) = lthy0
|> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
@@ -2115,7 +2115,7 @@
ks xss;
val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
+ #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Tue Mar 31 00:21:07 2015 +0200
@@ -382,7 +382,7 @@
in
(case b_opt of
NONE => ((t, Drule.dummy_thm), lthy)
- | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
+ | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []),
fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
end;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Tue Mar 31 00:21:07 2015 +0200
@@ -629,11 +629,13 @@
subtract (op =) Xs (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs) @ Xs;
fun raw_qualify base_b =
- let val (_, qs, n) = Binding.dest base_b;
+ let
+ val qs = Binding.path_of base_b;
+ val n = Binding.name_of base_b;
in
Binding.prefix_name rawN
#> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
- #> Binding.conceal
+ #> Binding.concealed
end;
val ((bnfs, (deadss, livess)), accum) =
@@ -643,7 +645,7 @@
((empty_comp_cache, empty_unfolds), lthy));
fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
- #> Binding.conceal;
+ #> Binding.concealed;
val Ass = map (map dest_TFree) livess;
val Ds' = fold (fold Term.add_tfreesT) deadss [];
@@ -660,7 +662,7 @@
val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
fun pre_qualify b = Binding.qualify false (Binding.name_of b)
- #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
+ #> not (Config.get lthy' bnf_note_all) ? Binding.concealed;
val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
@{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Tue Mar 31 00:21:07 2015 +0200
@@ -72,11 +72,11 @@
val b = Binding.name b_name;
fun mk_internal_of_b name =
- Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+ Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
fun mk_internal_b name = mk_internal_of_b name b;
fun mk_internal_bs name = map (mk_internal_of_b name) bs;
val external_bs = map2 (Binding.prefix false) b_names bs
- |> not note_all ? map Binding.conceal;
+ |> not note_all ? map Binding.concealed;
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -1317,7 +1317,7 @@
||>> mk_Frees' "rec" hrecTs;
fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
- val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
+ val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
fun dtor_spec rep str map_FT Jz Jz' =
Term.absfree Jz'
@@ -1364,7 +1364,7 @@
val timer = time (timer "dtor definitions & thms");
fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
- val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
+ val unfold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o unfold_bind;
fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z));
@@ -1456,7 +1456,7 @@
map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
- val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
+ val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
fun ctor_spec i = mk_unfold Ts map_dtors i;
@@ -1520,7 +1520,7 @@
end;
fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
- val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
+ val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind;
val corec_strs =
@{map 3} (fn dtor => fn sum_s => fn mapx =>
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Tue Mar 31 00:21:07 2015 +0200
@@ -984,7 +984,7 @@
|> map2 currys arg_Tss
|> (fn ts => Syntax.check_terms ctxt ts
handle ERROR _ => nonprimitive_corec ctxt [])
- |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+ |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
bs mxs
|> rpair excludess'
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Tue Mar 31 00:21:07 2015 +0200
@@ -42,11 +42,11 @@
val b = Binding.name b_name;
fun mk_internal_of_b name =
- Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
+ Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
fun mk_internal_b name = mk_internal_of_b name b;
fun mk_internal_bs name = map (mk_internal_of_b name) bs;
val external_bs = map2 (Binding.prefix false) b_names bs
- |> not note_all ? map Binding.conceal;
+ |> not note_all ? map Binding.concealed;
val deads = fold (union (op =)) Dss resDs;
val names_lthy = fold Variable.declare_typ deads lthy;
@@ -911,7 +911,7 @@
val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
- val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
+ val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
fun ctor_spec abs str map_FT_init =
Library.foldl1 HOLogic.mk_comp [abs, str,
@@ -965,7 +965,7 @@
val foldx = HOLogic.choice_const foldT $ fold_fun;
fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
- val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
+ val fold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o fold_bind;
fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
@@ -1072,7 +1072,7 @@
map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
- val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
+ val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
fun dtor_spec i = mk_fold Ts map_ctors i;
@@ -1135,7 +1135,7 @@
end;
fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
- val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
+ val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind;
val rec_strs =
@{map 3} (fn ctor => fn prod_s => fn mapx =>
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Tue Mar 31 00:21:07 2015 +0200
@@ -457,7 +457,7 @@
(recs, ctr_poss)
|-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
|> Syntax.check_terms ctxt
- |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
+ |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
bs mxs
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Mar 31 00:21:07 2015 +0200
@@ -175,7 +175,7 @@
#>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
val maybe_conceal_def_binding = Thm.def_binding
- #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
+ #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs [];
val size_Ts = map fastype_of size_rhss;
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Tue Mar 31 00:21:07 2015 +0200
@@ -142,10 +142,10 @@
fun typedef (b, Ts, mx) set opt_morphs tac lthy =
let
(*Work around loss of qualification in "typedef" axioms by replicating it in the name*)
- val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
+ val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
val ((name, info), (lthy, lthy_old)) =
lthy
- |> Local_Theory.conceal
+ |> Local_Theory.concealed
|> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
||> Local_Theory.restore_naming lthy
||> `Local_Theory.restore;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Tue Mar 31 00:21:07 2015 +0200
@@ -499,7 +499,7 @@
val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
|> Local_Theory.define ((case_binding, NoSyn),
- ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
+ ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs))
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy lthy';
--- a/src/HOL/Tools/Function/function.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Function/function.ML Tue Mar 31 00:21:07 2015 +0200
@@ -107,20 +107,20 @@
val fnames = map (fst o fst) fixes
fun qualify n = Binding.name n
|> Binding.qualify true defname
- val conceal_partial = if partials then I else Binding.conceal
+ val concealed_partial = if partials then I else Binding.concealed
val addsmps = add_simps fnames post sort_cont
val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
lthy
- |> addsmps (conceal_partial o Binding.qualify false "partial")
- "psimps" conceal_partial psimp_attribs psimps
- ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
+ |> addsmps (concealed_partial o Binding.qualify false "partial")
+ "psimps" concealed_partial psimp_attribs psimps
+ ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []),
simple_pinducts |> map (fn th => ([th],
[Attrib.internal (K (Rule_Cases.case_names cnames)),
Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
Attrib.internal (K (Induct.induct_pred ""))])))]
- ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
+ ||>> (apfst snd o Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]))
||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *)
||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims)
||> (case domintros of NONE => I | SOME thms =>
--- a/src/HOL/Tools/Function/function_core.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML Tue Mar 31 00:21:07 2015 +0200
@@ -445,7 +445,7 @@
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
lthy
- |> Local_Theory.conceal
+ |> Local_Theory.concealed
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
@@ -507,7 +507,7 @@
in
Local_Theory.define
((Binding.name (function_name fname), mixfix),
- ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
+ ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
end
fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
--- a/src/HOL/Tools/Function/mutual.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Tue Mar 31 00:21:07 2015 +0200
@@ -131,7 +131,7 @@
val ((f, (_, f_defthm)), lthy') =
Local_Theory.define
((Binding.name fname, mixfix),
- ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
+ ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
Term.subst_bound (fsum, f_def))) lthy
in
(MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
--- a/src/HOL/Tools/Function/partial_function.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Function/partial_function.ML Tue Mar 31 00:21:07 2015 +0200
@@ -262,7 +262,7 @@
val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
- val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
+ val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
val ((f, (_, f_def)), lthy') = Local_Theory.define
((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Tue Mar 31 00:21:07 2015 +0200
@@ -172,7 +172,7 @@
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
thy1
- |> Sign.map_naming Name_Space.conceal
+ |> Sign.map_naming Name_Space.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
coind = false, no_elim = true, no_ind = false, skip_mono = true}
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Tue Mar 31 00:21:07 2015 +0200
@@ -201,7 +201,7 @@
val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
(list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
- in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
+ in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end;
(* find datatypes which contain all datatypes in tnames' *)
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Tue Mar 31 00:21:07 2015 +0200
@@ -146,7 +146,7 @@
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
thy0
- |> Sign.map_naming Name_Space.conceal
+ |> Sign.map_naming Name_Space.concealed
|> Inductive.add_inductive_global
{quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
coind = false, no_elim = false, no_ind = true, skip_mono = true}
--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Tue Mar 31 00:21:07 2015 +0200
@@ -362,9 +362,9 @@
val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
in
Function.add_function
- (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
+ (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
(names ~~ Ts))
- (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
+ (map (pair (apfst Binding.concealed Attrib.empty_binding)) eqs_t)
Function_Common.default_config pat_completeness_auto
#> snd
#> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
@@ -372,8 +372,8 @@
end
else
fold_map (fn (name, T) => Local_Theory.define
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
+ ((Binding.concealed (Binding.name name), NoSyn),
+ (apfst Binding.concealed Attrib.empty_binding, mk_undefined T))
#> apfst fst) (names ~~ Ts)
#> (fn (consts, lthy) =>
let
--- a/src/HOL/Tools/Quickcheck/random_generators.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML Tue Mar 31 00:21:07 2015 +0200
@@ -97,7 +97,7 @@
val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
val ((_, (_, eqs2)), lthy') = lthy
|> BNF_LFP_Compat.add_primrec_simple
- [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
+ [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
val cT_random_aux = inst pt_random_aux;
val cT_rhs = inst pt_rhs;
val rule = @{thm random_aux_rec}
@@ -136,8 +136,8 @@
val projs = mk_proj (aux_lhs) Ts;
val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
- ((Binding.conceal (Binding.name name), NoSyn),
- (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
+ ((Binding.concealed (Binding.name name), NoSyn),
+ (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs;
val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
fun prove_eqs aux_simp proj_defs lthy =
let
@@ -168,7 +168,7 @@
val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
- val b = Binding.conceal (Binding.qualify true prfx
+ val b = Binding.concealed (Binding.qualify true prfx
(Binding.qualify true name (Binding.name "simps")));
in
lthy
@@ -262,7 +262,7 @@
|> random_aux_specification prfx random_auxN auxs_eqs
|> `(fn lthy => map (Syntax.check_term lthy) random_defs)
|-> (fn random_defs' => fold_map (fn random_def =>
- Specification.definition (NONE, (apfst Binding.conceal
+ Specification.definition (NONE, (apfst Binding.concealed
Attrib.empty_binding, random_def))) random_defs')
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
--- a/src/HOL/Tools/inductive.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/inductive.ML Tue Mar 31 00:21:07 2015 +0200
@@ -843,10 +843,10 @@
val is_auxiliary = length cs >= 2;
val ((rec_const, (_, fp_def)), lthy') = lthy
- |> is_auxiliary ? Local_Theory.conceal
+ |> is_auxiliary ? Local_Theory.concealed
|> Local_Theory.define
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
- ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
+ ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
fold_rev lambda params
(Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
||> is_auxiliary ? Local_Theory.restore_naming lthy;
@@ -862,7 +862,7 @@
val xs =
map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
in
- (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
+ (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
(list_comb (rec_const, params @ make_bool_args' bs i @
make_args argTs (xs ~~ Ts)))))
end) (cnames_syn ~~ cs);
@@ -873,7 +873,7 @@
val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
val (_, lthy'''') =
- Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
+ Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
Proof_Context.export lthy''' lthy'' [mono]) lthy'';
in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
--- a/src/HOL/Tools/inductive_set.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/inductive_set.ML Tue Mar 31 00:21:07 2015 +0200
@@ -488,7 +488,7 @@
(* define inductive sets using previously defined predicates *)
val (defs, lthy2) = lthy1
- |> Local_Theory.conceal (* FIXME ?? *)
+ |> Local_Theory.concealed (* FIXME ?? *)
|> fold_map Local_Theory.define
(map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
fold_rev lambda params (HOLogic.Collect_const U $
--- a/src/HOL/Tools/recdef.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/recdef.ML Tue Mar 31 00:21:07 2015 +0200
@@ -260,7 +260,7 @@
" in recdef definition of " ^ quote name);
in
Specification.theorem "" NONE (K I)
- (Binding.conceal (Binding.name bname), atts) [] []
+ (Binding.concealed (Binding.name bname), atts) [] []
(Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
--- a/src/HOL/Tools/record.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/record.ML Tue Mar 31 00:21:07 2015 +0200
@@ -152,7 +152,7 @@
typ_thy
|> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
|> Global_Theory.add_defs false
- [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
+ [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
@@ -1720,7 +1720,7 @@
thy
|> Class.instantiation ([tyco], vs, sort)
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
+ |-> (fn eq => Specification.definition (NONE, (apfst Binding.concealed Attrib.empty_binding, eq)))
|> snd
|> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
end;
@@ -2017,12 +2017,12 @@
|> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
|> (Global_Theory.add_defs false o
- map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
+ map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
||>> (Global_Theory.add_defs false o
- map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
+ map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
||>> (Global_Theory.add_defs false o
map (rpair [Code.add_default_eqn_attribute]
- o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
+ o apfst (Binding.concealed o Binding.name))) (*FIXME Spec_Rules (?)*)
[make_spec, fields_spec, extend_spec, truncate_spec]);
val defs_ctxt = Proof_Context.init_global defs_thy;
--- a/src/HOL/Tools/typedef.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/HOL/Tools/typedef.ML Tue Mar 31 00:21:07 2015 +0200
@@ -137,9 +137,9 @@
(* prepare_typedef *)
-fun prepare_typedef conceal prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
+fun prepare_typedef concealed prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
let
- val concealed_name = name |> conceal ? Binding.conceal;
+ val concealed_name = name |> concealed ? Binding.concealed;
val bname = Binding.name_of name;
@@ -242,18 +242,18 @@
(* add_typedef: tactic interface *)
-fun add_typedef conceal typ set opt_morphs tac lthy =
+fun add_typedef concealed typ set opt_morphs tac lthy =
let
val ((goal, _, typedef_result), lthy') =
- prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy;
+ prepare_typedef concealed Syntax.check_term typ set opt_morphs lthy;
val inhabited =
Goal.prove lthy' [] [] goal (tac o #context)
|> Goal.norm_result lthy' |> Thm.close_derivation;
in typedef_result inhabited lthy' end;
-fun add_typedef_global conceal typ set opt_morphs tac =
+fun add_typedef_global concealed typ set opt_morphs tac =
Named_Target.theory_init
- #> add_typedef conceal typ set opt_morphs tac
+ #> add_typedef concealed typ set opt_morphs tac
#> Local_Theory.exit_result_global (apsnd o transform_info);
--- a/src/Pure/General/binding.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/General/binding.ML Tue Mar 31 00:21:07 2015 +0200
@@ -10,7 +10,8 @@
signature BINDING =
sig
eqtype binding
- val dest: binding -> bool * (string * bool) list * bstring
+ val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
+ val path_of: binding -> (string * bool) list
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
val set_pos: Position.T -> binding -> binding
@@ -28,7 +29,8 @@
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
- val conceal: binding -> binding
+ val private: binding -> binding
+ val concealed: binding -> binding
val pretty: binding -> Pretty.T
val print: binding -> string
val pp: binding -> Pretty.T
@@ -44,20 +46,24 @@
(* datatype *)
datatype binding = Binding of
- {conceal: bool, (*internal -- for foundational purposes only*)
+ {private: bool, (*entry is strictly private -- no name space accesses*)
+ concealed: bool, (*entry is for foundational purposes -- please ignore*)
prefix: (string * bool) list, (*system prefix*)
qualifier: (string * bool) list, (*user qualifier*)
name: bstring, (*base name*)
pos: Position.T}; (*source position*)
-fun make_binding (conceal, prefix, qualifier, name, pos) =
- Binding {conceal = conceal, prefix = prefix, qualifier = qualifier, name = name, pos = pos};
+fun make_binding (private, concealed, prefix, qualifier, name, pos) =
+ Binding {private = private, concealed = concealed, prefix = prefix,
+ qualifier = qualifier, name = name, pos = pos};
-fun map_binding f (Binding {conceal, prefix, qualifier, name, pos}) =
- make_binding (f (conceal, prefix, qualifier, name, pos));
+fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
+ make_binding (f (private, concealed, prefix, qualifier, name, pos));
-fun dest (Binding {conceal, prefix, qualifier, name, ...}) =
- (conceal, prefix @ qualifier, name);
+fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
+ {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
+
+val path_of = #path o dest;
@@ -65,11 +71,12 @@
(* name and position *)
-fun make (name, pos) = make_binding (false, [], [], name, pos);
+fun make (name, pos) = make_binding (false, false, [], [], name, pos);
fun pos_of (Binding {pos, ...}) = pos;
fun set_pos pos =
- map_binding (fn (conceal, prefix, qualifier, name, _) => (conceal, prefix, qualifier, name, pos));
+ map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
+ (private, concealed, prefix, qualifier, name, pos));
fun name name = make (name, Position.none);
fun name_of (Binding {name, ...}) = name;
@@ -77,8 +84,8 @@
fun eq_name (b, b') = name_of b = name_of b';
fun map_name f =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, prefix, qualifier, f name, pos));
+ map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ (private, concealed, prefix, qualifier, f name, pos));
val prefix_name = map_name o prefix;
val suffix_name = map_name o suffix;
@@ -91,17 +98,18 @@
fun qualify _ "" = I
| qualify mandatory qual =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
+ map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
-fun qualified mandatory name' = map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
- in (conceal, prefix, qualifier', name', pos) end);
+fun qualified mandatory name' =
+ map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
+ in (private, concealed, prefix, qualifier', name', pos) end);
fun qualified_name "" = empty
| qualified_name s =
let val (qualifier, name) = split_last (Long_Name.explode s)
- in make_binding (false, [], map (rpair false) qualifier, name, Position.none) end;
+ in make_binding (false, false, [], map (rpair false) qualifier, name, Position.none) end;
(* system prefix *)
@@ -109,18 +117,22 @@
fun prefix_of (Binding {prefix, ...}) = prefix;
fun map_prefix f =
- map_binding (fn (conceal, prefix, qualifier, name, pos) =>
- (conceal, f prefix, qualifier, name, pos));
+ map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
+ (private, concealed, f prefix, qualifier, name, pos));
fun prefix _ "" = I
| prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
-(* conceal *)
+(* visibility flags *)
-val conceal =
- map_binding (fn (_, prefix, qualifier, name, pos) =>
- (true, prefix, qualifier, name, pos));
+val private =
+ map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
+ (true, concealed, prefix, qualifier, name, pos));
+
+val concealed =
+ map_binding (fn (private, _, prefix, qualifier, name, pos) =>
+ (private, true, prefix, qualifier, name, pos));
(* print *)
@@ -148,4 +160,3 @@
end;
type binding = Binding.binding;
-
--- a/src/Pure/General/name_space.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/General/name_space.ML Tue Mar 31 00:21:07 2015 +0200
@@ -33,7 +33,8 @@
val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
val merge: T * T -> T
type naming
- val conceal: naming -> naming
+ val private: naming -> naming
+ val concealed: naming -> naming
val get_group: naming -> serial option
val set_group: serial option -> naming -> naming
val set_theory_name: string -> naming -> naming
@@ -283,32 +284,37 @@
(* datatype naming *)
datatype naming = Naming of
- {conceal: bool,
+ {private: bool,
+ concealed: bool,
group: serial option,
theory_name: string,
path: (string * bool) list};
-fun make_naming (conceal, group, theory_name, path) =
- Naming {conceal = conceal, group = group, theory_name = theory_name, path = path};
+fun make_naming (private, concealed, group, theory_name, path) =
+ Naming {private = private, concealed = concealed, group = group,
+ theory_name = theory_name, path = path};
-fun map_naming f (Naming {conceal, group, theory_name, path}) =
- make_naming (f (conceal, group, theory_name, path));
+fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
+ make_naming (f (private, concealed, group, theory_name, path));
-fun map_path f = map_naming (fn (conceal, group, theory_name, path) =>
- (conceal, group, theory_name, f path));
+fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
+ (private, concealed, group, theory_name, f path));
-val conceal = map_naming (fn (_, group, theory_name, path) =>
- (true, group, theory_name, path));
+val private = map_naming (fn (_, concealed, group, theory_name, path) =>
+ (true, concealed, group, theory_name, path));
-fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
- (conceal, group, theory_name, path));
+val concealed = map_naming (fn (private, _, group, theory_name, path) =>
+ (private, true, group, theory_name, path));
+
+fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
+ (private, concealed, group, theory_name, path));
fun get_group (Naming {group, ...}) = group;
-fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
- (conceal, group, theory_name, path));
+fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
+ (private, concealed, group, theory_name, path));
fun new_group naming = set_group (SOME (serial ())) naming;
val reset_group = set_group NONE;
@@ -319,9 +325,9 @@
fun mandatory_path elems = map_path (fn path => path @ [(elems, true)]);
fun qualified_path mandatory binding = map_path (fn path =>
- path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
+ path @ Binding.path_of (Binding.qualified mandatory "" binding));
-val global_naming = make_naming (false, NONE, "", []);
+val global_naming = make_naming (false, false, NONE, "", []);
val local_naming = global_naming |> add_path Long_Name.localN;
@@ -329,27 +335,28 @@
fun err_bad binding = error (Binding.bad binding);
-fun transform_binding (Naming {conceal = true, ...}) = Binding.conceal
- | transform_binding _ = I;
+fun transform_binding (Naming {private, concealed, ...}) =
+ private ? Binding.private #>
+ concealed ? Binding.concealed;
val bad_specs = ["", "??", "__"];
-fun name_spec (naming as Naming {path, ...}) raw_binding =
+fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
let
val binding = transform_binding naming raw_binding;
- val (concealed, prefix, name) = Binding.dest binding;
+ val {private, concealed, path = path2, name} = Binding.dest binding;
val _ = Long_Name.is_qualified name andalso err_bad binding;
- val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
+ val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
val spec2 = if name = "" then [] else [(name, true)];
val spec = spec1 @ spec2;
val _ =
exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
andalso err_bad binding;
- in (concealed, if null spec2 then [] else spec) end;
+ in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
fun full_name naming =
- name_spec naming #> #2 #> map #1 #> Long_Name.implode;
+ name_spec naming #> #spec #> map #1 #> Long_Name.implode;
val base_name = full_name global_naming #> Long_Name.base_name;
@@ -366,11 +373,13 @@
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
fun accesses naming binding =
- let
- val spec = #2 (name_spec naming binding);
- val sfxs = mandatory_suffixes spec;
- val pfxs = mandatory_prefixes spec;
- in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
+ (case name_spec naming binding of
+ {private = true, ...} => ([], [])
+ | {spec, ...} =>
+ let
+ val sfxs = mandatory_suffixes spec;
+ val pfxs = mandatory_prefixes spec;
+ in apply2 (map Long_Name.implode) (sfxs @ pfxs, sfxs) end);
(* hide *)
@@ -433,7 +442,7 @@
let
val naming = naming_of context;
val Naming {group, theory_name, ...} = naming;
- val (concealed, spec) = name_spec naming binding;
+ val {concealed, spec, ...} = name_spec naming binding;
val (accs, accs') = accesses naming binding;
val name = Long_Name.implode (map fst spec);
@@ -556,4 +565,3 @@
fun markup_table ctxt (Table (space, tab)) = markup_entries ctxt space (Change_Table.dest tab);
end;
-
--- a/src/Pure/Isar/args.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/Isar/args.ML Tue Mar 31 00:21:07 2015 +0200
@@ -23,6 +23,7 @@
val maybe: 'a parser -> 'a option parser
val cartouche_inner_syntax: string parser
val cartouche_input: Input.source parser
+ val text_token: Token.T parser
val text_input: Input.source parser
val text: string parser
val name_inner_syntax: string parser
--- a/src/Pure/Isar/expression.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/Isar/expression.ML Tue Mar 31 00:21:07 2015 +0200
@@ -674,9 +674,9 @@
val ([pred_def], defs_thy) =
thy
|> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
- |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
+ |> Sign.declare_const_global ((Binding.concealed binding, predT), NoSyn) |> snd
|> Global_Theory.add_defs false
- [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
+ [((Binding.concealed (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
val intro = Goal.prove_global defs_thy [] norm_ts statement
@@ -721,7 +721,7 @@
thy'
|> Sign.qualified_path true abinding
|> Global_Theory.note_thmss ""
- [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
+ [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
val (b_pred, b_intro, b_axioms, thy'''') =
@@ -736,8 +736,8 @@
thy'''
|> Sign.qualified_path true binding
|> Global_Theory.note_thmss ""
- [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
- ((Binding.conceal (Binding.name axiomsN), []),
+ [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.intro_add])]),
+ ((Binding.concealed (Binding.name axiomsN), []),
[(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
[])])]
||> Sign.restore_naming thy''';
@@ -806,7 +806,7 @@
val notes =
if is_some asm then
- [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
+ [("", [((Binding.concealed (Binding.suffix_name ("_" ^ axiomsN) binding), []),
[([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
[(Attrib.internal o K) Locale.witness_add])])])]
else [];
--- a/src/Pure/Isar/local_theory.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/Isar/local_theory.ML Tue Mar 31 00:21:07 2015 +0200
@@ -28,7 +28,7 @@
val naming_of: local_theory -> Name_Space.naming
val full_name: local_theory -> binding -> string
val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
- val conceal: local_theory -> local_theory
+ val concealed: local_theory -> local_theory
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
val restore_naming: local_theory -> local_theory -> local_theory
@@ -188,7 +188,7 @@
map_top (fn (naming, operations, after_close, brittle, target) =>
(f naming, operations, after_close, brittle, target));
-val conceal = map_naming Name_Space.conceal;
+val concealed = map_naming Name_Space.concealed;
val new_group = map_naming Name_Space.new_group;
val reset_group = map_naming Name_Space.reset_group;
--- a/src/Pure/Isar/locale.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/Isar/locale.ML Tue Mar 31 00:21:07 2015 +0200
@@ -592,7 +592,7 @@
fun add_decl loc decl =
add_thmss loc ""
- [((Binding.conceal Binding.empty,
+ [((Binding.concealed Binding.empty,
[Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
[([Drule.dummy_thm], [])])];
--- a/src/Pure/Isar/proof_context.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/Isar/proof_context.ML Tue Mar 31 00:21:07 2015 +0200
@@ -1195,7 +1195,7 @@
(Name_Space.del_table name cases, index)
| update_case context is_proper (name, SOME c) (cases, index) =
let
- val binding = Binding.name name |> not is_proper ? Binding.conceal;
+ val binding = Binding.name name |> not is_proper ? Binding.concealed;
val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
val index' = index + 1;
in (cases', index') end;
--- a/src/Pure/axclass.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/axclass.ML Tue Mar 31 00:21:07 2015 +0200
@@ -362,7 +362,7 @@
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> apsnd Thm.varifyT_global
#-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
- #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
+ #> Global_Theory.add_thm ((Binding.concealed (Binding.name c'), thm), [])
#> #2
#> pair (Const (c, T))))
||> Sign.restore_naming thy
@@ -392,7 +392,7 @@
val rel = Logic.dest_classrel prop handle TERM _ => err ();
val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
val binding =
- Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
+ Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val th'' = th'
|> Thm.unconstrainT
@@ -413,7 +413,7 @@
val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
val binding =
- Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
+ Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
val (th', thy') = Global_Theory.store_thm (binding, th) thy;
val args = Name.invent_names Name.context Name.aT Ss;
--- a/src/Pure/drule.ML Mon Mar 30 20:59:14 2015 +0200
+++ b/src/Pure/drule.ML Tue Mar 31 00:21:07 2015 +0200
@@ -599,11 +599,11 @@
val protect = Thm.apply (certify Logic.protectC);
val protectI =
- store_standard_thm (Binding.conceal (Binding.make ("protectI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("protectI", @{here})))
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
val protectD =
- store_standard_thm (Binding.conceal (Binding.make ("protectD", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("protectD", @{here})))
(Thm.equal_elim prop_def (Thm.assume (protect A)));
val protect_cong =
@@ -622,7 +622,7 @@
(* term *)
val termI =
- store_standard_thm (Binding.conceal (Binding.make ("termI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("termI", @{here})))
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
fun mk_term ct =
@@ -648,11 +648,11 @@
(* sort_constraint *)
val sort_constraintI =
- store_standard_thm (Binding.conceal (Binding.make ("sort_constraintI", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
val sort_constraint_eq =
- store_standard_thm (Binding.conceal (Binding.make ("sort_constraint_eq", @{here})))
+ store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
(Thm.unvarify_global sort_constraintI)))