tuned signature;
authorwenzelm
Tue Mar 31 00:11:54 2015 +0200 (2015-03-31)
changeset 59859f9d1442c70f3
parent 59858 890b68e1e8b6
child 59860 a979fc5db526
tuned signature;
src/Doc/Implementation/Prelim.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Tools/BNF/bnf_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Function/function_core.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/partial_function.ML
src/HOL/Tools/Old_Datatype/old_datatype.ML
src/HOL/Tools/Old_Datatype/old_primrec.ML
src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
src/HOL/Tools/Quickcheck/quickcheck_common.ML
src/HOL/Tools/Quickcheck/random_generators.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/Pure/General/binding.ML
src/Pure/General/name_space.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/proof_context.ML
src/Pure/axclass.ML
src/Pure/drule.ML
     1.1 --- a/src/Doc/Implementation/Prelim.thy	Mon Mar 30 22:34:59 2015 +0200
     1.2 +++ b/src/Doc/Implementation/Prelim.thy	Tue Mar 31 00:11:54 2015 +0200
     1.3 @@ -917,7 +917,7 @@
     1.4    @{index_ML Binding.name: "string -> binding"} \\
     1.5    @{index_ML Binding.qualify: "bool -> string -> binding -> binding"} \\
     1.6    @{index_ML Binding.prefix: "bool -> string -> binding -> binding"} \\
     1.7 -  @{index_ML Binding.conceal: "binding -> binding"} \\
     1.8 +  @{index_ML Binding.concealed: "binding -> binding"} \\
     1.9    @{index_ML Binding.print: "binding -> string"} \\
    1.10    \end{mldecls}
    1.11    \begin{mldecls}
    1.12 @@ -961,7 +961,7 @@
    1.13    typically used in the infrastructure for modular specifications,
    1.14    notably ``local theory targets'' (see also \chref{ch:local-theory}).
    1.15  
    1.16 -  \item @{ML Binding.conceal}~@{text "binding"} indicates that the
    1.17 +  \item @{ML Binding.concealed}~@{text "binding"} indicates that the
    1.18    binding shall refer to an entity that serves foundational purposes
    1.19    only.  This flag helps to mark implementation details of
    1.20    specification mechanism etc.  Other tools should not depend on the
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Mar 30 22:34:59 2015 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Mar 31 00:11:54 2015 +0200
     2.3 @@ -529,7 +529,7 @@
     2.4  
     2.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
     2.6        thy3
     2.7 -      |> Sign.map_naming Name_Space.conceal
     2.8 +      |> Sign.map_naming Name_Space.concealed
     2.9        |> Inductive.add_inductive_global
    2.10            {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
    2.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    2.12 @@ -1505,7 +1505,7 @@
    2.13  
    2.14      val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
    2.15        thy10
    2.16 -      |> Sign.map_naming Name_Space.conceal
    2.17 +      |> Sign.map_naming Name_Space.concealed
    2.18        |> Inductive.add_inductive_global
    2.19            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    2.20             coind = false, no_elim = false, no_ind = false, skip_mono = true}
     3.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Mar 30 22:34:59 2015 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Tue Mar 31 00:11:54 2015 +0200
     3.3 @@ -899,7 +899,7 @@
     3.4  
     3.5      val bnf_b = qualify b;
     3.6      val def_qualify =
     3.7 -      Thm.def_binding o Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
     3.8 +      Thm.def_binding o Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
     3.9      fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
    3.10      val map_b = def_qualify (mk_prefix_binding mapN);
    3.11      val rel_b = def_qualify (mk_prefix_binding relN);
     4.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Mon Mar 30 22:34:59 2015 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Tue Mar 31 00:11:54 2015 +0200
     4.3 @@ -765,7 +765,7 @@
     4.4    let
     4.5      val live = length set_rhss;
     4.6  
     4.7 -    val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
     4.8 +    val def_qualify = Binding.concealed o Binding.qualify false (Binding.name_of bnf_b);
     4.9  
    4.10      fun mk_prefix_binding pre = Binding.prefix_name (pre ^ "_") bnf_b;
    4.11  
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 30 22:34:59 2015 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Mar 31 00:11:54 2015 +0200
     5.3 @@ -1218,7 +1218,7 @@
     5.4      val thy = Proof_Context.theory_of lthy0;
     5.5  
     5.6      val maybe_conceal_def_binding = Thm.def_binding
     5.7 -      #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
     5.8 +      #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
     5.9  
    5.10      val ((cst, (_, def)), (lthy', lthy)) = lthy0
    5.11        |> Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
    5.12 @@ -2115,7 +2115,7 @@
    5.13              ks xss;
    5.14  
    5.15          val maybe_conceal_def_binding = Thm.def_binding
    5.16 -          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.conceal;
    5.17 +          #> not (Config.get no_defs_lthy bnf_note_all) ? Binding.concealed;
    5.18  
    5.19          val ((raw_ctrs, raw_ctr_defs), (lthy', lthy)) = no_defs_lthy
    5.20            |> apfst split_list o @{fold_map 3} (fn b => fn mx => fn rhs =>
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Mon Mar 30 22:34:59 2015 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Tue Mar 31 00:11:54 2015 +0200
     6.3 @@ -382,7 +382,7 @@
     6.4        in
     6.5          (case b_opt of
     6.6            NONE => ((t, Drule.dummy_thm), lthy)
     6.7 -        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []),
     6.8 +        | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.concealed (Thm.def_binding b), []),
     6.9              fold_rev Term.absfree rec_strs' t)) lthy |>> apsnd snd)
    6.10        end;
    6.11  
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Mar 30 22:34:59 2015 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 31 00:11:54 2015 +0200
     7.3 @@ -619,7 +619,7 @@
     7.4        in
     7.5          Binding.prefix_name rawN
     7.6          #> fold_rev (fn (s, mand) => Binding.qualify mand s) (qs @ [(n, true)])
     7.7 -        #> Binding.conceal
     7.8 +        #> Binding.concealed
     7.9        end;
    7.10  
    7.11      val ((bnfs, (deadss, livess)), accum) =
    7.12 @@ -629,7 +629,7 @@
    7.13            ((empty_comp_cache, empty_unfolds), lthy));
    7.14  
    7.15      fun norm_qualify i = Binding.qualify true (Binding.name_of (nth bs (Int.max (0, i - 1))))
    7.16 -      #> Binding.conceal;
    7.17 +      #> Binding.concealed;
    7.18  
    7.19      val Ass = map (map dest_TFree) livess;
    7.20      val Ds' = fold (fold Term.add_tfreesT) deadss [];
    7.21 @@ -646,7 +646,7 @@
    7.22      val Dss = @{map 3} (uncurry append oo curry swap oo map o nth) livess kill_poss deadss;
    7.23  
    7.24      fun pre_qualify b = Binding.qualify false (Binding.name_of b)
    7.25 -      #> not (Config.get lthy' bnf_note_all) ? Binding.conceal;
    7.26 +      #> not (Config.get lthy' bnf_note_all) ? Binding.concealed;
    7.27  
    7.28      val ((pre_bnfs, (deadss, absT_infos)), lthy'') =
    7.29        @{fold_map 4} (fn b => seal_bnf (pre_qualify b) unfold_set' (Binding.prefix_name preN b))
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 30 22:34:59 2015 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Tue Mar 31 00:11:54 2015 +0200
     8.3 @@ -72,11 +72,11 @@
     8.4      val b = Binding.name b_name;
     8.5  
     8.6      fun mk_internal_of_b name =
     8.7 -      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
     8.8 +      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
     8.9      fun mk_internal_b name = mk_internal_of_b name b;
    8.10      fun mk_internal_bs name = map (mk_internal_of_b name) bs;
    8.11      val external_bs = map2 (Binding.prefix false) b_names bs
    8.12 -      |> not note_all ? map Binding.conceal;
    8.13 +      |> not note_all ? map Binding.concealed;
    8.14  
    8.15      val deads = fold (union (op =)) Dss resDs;
    8.16      val names_lthy = fold Variable.declare_typ deads lthy;
    8.17 @@ -1317,7 +1317,7 @@
    8.18        ||>> mk_Frees' "rec" hrecTs;
    8.19  
    8.20      fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
    8.21 -    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
    8.22 +    val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
    8.23  
    8.24      fun dtor_spec rep str map_FT Jz Jz' =
    8.25        Term.absfree Jz'
    8.26 @@ -1364,7 +1364,7 @@
    8.27      val timer = time (timer "dtor definitions & thms");
    8.28  
    8.29      fun unfold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_unfoldN ^ "_");
    8.30 -    val unfold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o unfold_bind;
    8.31 +    val unfold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o unfold_bind;
    8.32  
    8.33      fun unfold_spec abs f z = fold_rev (Term.absfree o Term.dest_Free) (ss @ [z]) (abs $ (f $ z));
    8.34  
    8.35 @@ -1456,7 +1456,7 @@
    8.36          map HOLogic.id_const passiveAs @ dtors)) Dss bnfs;
    8.37  
    8.38      fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
    8.39 -    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
    8.40 +    val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
    8.41  
    8.42      fun ctor_spec i = mk_unfold Ts map_dtors i;
    8.43  
    8.44 @@ -1520,7 +1520,7 @@
    8.45        end;
    8.46  
    8.47      fun corec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtor_corecN ^ "_");
    8.48 -    val corec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o corec_bind;
    8.49 +    val corec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o corec_bind;
    8.50  
    8.51      val corec_strs =
    8.52        @{map 3} (fn dtor => fn sum_s => fn mapx =>
     9.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Mon Mar 30 22:34:59 2015 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 31 00:11:54 2015 +0200
     9.3 @@ -984,7 +984,7 @@
     9.4      |> map2 currys arg_Tss
     9.5      |> (fn ts => Syntax.check_terms ctxt ts
     9.6        handle ERROR _ => nonprimitive_corec ctxt [])
     9.7 -    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
     9.8 +    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
     9.9        bs mxs
    9.10      |> rpair excludess'
    9.11    end;
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Mar 30 22:34:59 2015 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Tue Mar 31 00:11:54 2015 +0200
    10.3 @@ -42,11 +42,11 @@
    10.4      val b = Binding.name b_name;
    10.5  
    10.6      fun mk_internal_of_b name =
    10.7 -      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.conceal;
    10.8 +      Binding.prefix_name (name ^ "_") #> Binding.prefix true b_name #> Binding.concealed;
    10.9      fun mk_internal_b name = mk_internal_of_b name b;
   10.10      fun mk_internal_bs name = map (mk_internal_of_b name) bs;
   10.11      val external_bs = map2 (Binding.prefix false) b_names bs
   10.12 -      |> not note_all ? map Binding.conceal;
   10.13 +      |> not note_all ? map Binding.concealed;
   10.14  
   10.15      val deads = fold (union (op =)) Dss resDs;
   10.16      val names_lthy = fold Variable.declare_typ deads lthy;
   10.17 @@ -911,7 +911,7 @@
   10.18      val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis;
   10.19  
   10.20      fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_");
   10.21 -    val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind;
   10.22 +    val ctor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o ctor_bind;
   10.23  
   10.24      fun ctor_spec abs str map_FT_init =
   10.25        Library.foldl1 HOLogic.mk_comp [abs, str,
   10.26 @@ -965,7 +965,7 @@
   10.27      val foldx = HOLogic.choice_const foldT $ fold_fun;
   10.28  
   10.29      fun fold_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_foldN ^ "_");
   10.30 -    val fold_def_bind = rpair [] o Binding.conceal o Thm.def_binding o fold_bind;
   10.31 +    val fold_def_bind = rpair [] o Binding.concealed o Thm.def_binding o fold_bind;
   10.32  
   10.33      fun fold_spec i = fold_rev (Term.absfree o Term.dest_Free) ss (mk_nthN n foldx i);
   10.34  
   10.35 @@ -1072,7 +1072,7 @@
   10.36          map HOLogic.id_const passiveAs @ ctors)) Dss bnfs;
   10.37  
   10.38      fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
   10.39 -    val dtor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o dtor_bind;
   10.40 +    val dtor_def_bind = rpair [] o Binding.concealed o Thm.def_binding o dtor_bind;
   10.41  
   10.42      fun dtor_spec i = mk_fold Ts map_ctors i;
   10.43  
   10.44 @@ -1135,7 +1135,7 @@
   10.45        end;
   10.46  
   10.47      fun rec_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctor_recN ^ "_");
   10.48 -    val rec_def_bind = rpair [] o Binding.conceal o Thm.def_binding o rec_bind;
   10.49 +    val rec_def_bind = rpair [] o Binding.concealed o Thm.def_binding o rec_bind;
   10.50  
   10.51      val rec_strs =
   10.52        @{map 3} (fn ctor => fn prod_s => fn mapx =>
    11.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Mon Mar 30 22:34:59 2015 +0200
    11.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Mar 31 00:11:54 2015 +0200
    11.3 @@ -457,7 +457,7 @@
    11.4      (recs, ctr_poss)
    11.5      |-> map2 (fn recx => fn ctr_pos => list_comb (recx, rec_args) |> permute_args ctr_pos)
    11.6      |> Syntax.check_terms ctxt
    11.7 -    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.conceal (Thm.def_binding b), []), t)))
    11.8 +    |> @{map 3} (fn b => fn mx => fn t => ((b, mx), ((Binding.concealed (Thm.def_binding b), []), t)))
    11.9        bs mxs
   11.10    end;
   11.11  
    12.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Mar 30 22:34:59 2015 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Tue Mar 31 00:11:54 2015 +0200
    12.3 @@ -175,7 +175,7 @@
    12.4          #>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)));
    12.5  
    12.6        val maybe_conceal_def_binding = Thm.def_binding
    12.7 -        #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal;
    12.8 +        #> not (Config.get lthy0 bnf_note_all) ? Binding.concealed;
    12.9  
   12.10        val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs [];
   12.11        val size_Ts = map fastype_of size_rhss;
    13.1 --- a/src/HOL/Tools/BNF/bnf_util.ML	Mon Mar 30 22:34:59 2015 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_util.ML	Tue Mar 31 00:11:54 2015 +0200
    13.3 @@ -145,7 +145,7 @@
    13.4      val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (Binding.path_of b)) b;
    13.5      val ((name, info), (lthy, lthy_old)) =
    13.6        lthy
    13.7 -      |> Local_Theory.conceal
    13.8 +      |> Local_Theory.concealed
    13.9        |> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
   13.10        ||> Local_Theory.restore_naming lthy
   13.11        ||> `Local_Theory.restore;
    14.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Mar 30 22:34:59 2015 +0200
    14.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Tue Mar 31 00:11:54 2015 +0200
    14.3 @@ -499,7 +499,7 @@
    14.4  
    14.5      val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy
    14.6        |> Local_Theory.define ((case_binding, NoSyn),
    14.7 -        ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs))
    14.8 +        ((Binding.concealed (Thm.def_binding case_binding), []), case_rhs))
    14.9        ||> `Local_Theory.restore;
   14.10  
   14.11      val phi = Proof_Context.export_morphism lthy lthy';
    15.1 --- a/src/HOL/Tools/Function/function.ML	Mon Mar 30 22:34:59 2015 +0200
    15.2 +++ b/src/HOL/Tools/Function/function.ML	Tue Mar 31 00:11:54 2015 +0200
    15.3 @@ -107,20 +107,20 @@
    15.4          val fnames = map (fst o fst) fixes
    15.5          fun qualify n = Binding.name n
    15.6            |> Binding.qualify true defname
    15.7 -        val conceal_partial = if partials then I else Binding.conceal
    15.8 +        val concealed_partial = if partials then I else Binding.concealed
    15.9  
   15.10          val addsmps = add_simps fnames post sort_cont
   15.11  
   15.12          val (((((psimps', [pinducts']), [termination']), cases'), pelims'), lthy) =
   15.13            lthy
   15.14 -          |> addsmps (conceal_partial o Binding.qualify false "partial")
   15.15 -               "psimps" conceal_partial psimp_attribs psimps
   15.16 -          ||>> Local_Theory.notes [((conceal_partial (qualify "pinduct"), []),
   15.17 +          |> addsmps (concealed_partial o Binding.qualify false "partial")
   15.18 +               "psimps" concealed_partial psimp_attribs psimps
   15.19 +          ||>> Local_Theory.notes [((concealed_partial (qualify "pinduct"), []),
   15.20                  simple_pinducts |> map (fn th => ([th],
   15.21                   [Attrib.internal (K (Rule_Cases.case_names cnames)),
   15.22                    Attrib.internal (K (Rule_Cases.consumes (1 - Thm.nprems_of th))),
   15.23                    Attrib.internal (K (Induct.induct_pred ""))])))]
   15.24 -          ||>> (apfst snd o Local_Theory.note ((Binding.conceal (qualify "termination"), []), [termination]))
   15.25 +          ||>> (apfst snd o Local_Theory.note ((Binding.concealed (qualify "termination"), []), [termination]))
   15.26            ||>> fold_map (note_qualified "cases" [Rule_Cases.case_names cnames]) (fnames ~~ map single cases) (* TODO: case names *)
   15.27            ||>> fold_map (note_qualified "pelims" [Rule_Cases.consumes 1, Rule_Cases.constraints 1]) (fnames ~~ pelims)
   15.28            ||> (case domintros of NONE => I | SOME thms =>
    16.1 --- a/src/HOL/Tools/Function/function_core.ML	Mon Mar 30 22:34:59 2015 +0200
    16.2 +++ b/src/HOL/Tools/Function/function_core.ML	Tue Mar 31 00:11:54 2015 +0200
    16.3 @@ -445,7 +445,7 @@
    16.4    let
    16.5      val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
    16.6        lthy
    16.7 -      |> Local_Theory.conceal
    16.8 +      |> Local_Theory.concealed
    16.9        |> Inductive.add_inductive_i
   16.10            {quiet_mode = true,
   16.11              verbose = ! trace,
   16.12 @@ -507,7 +507,7 @@
   16.13    in
   16.14      Local_Theory.define
   16.15        ((Binding.name (function_name fname), mixfix),
   16.16 -        ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   16.17 +        ((Binding.concealed (Binding.name fdefname), []), f_def)) lthy
   16.18    end
   16.19  
   16.20  fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
    17.1 --- a/src/HOL/Tools/Function/mutual.ML	Mon Mar 30 22:34:59 2015 +0200
    17.2 +++ b/src/HOL/Tools/Function/mutual.ML	Tue Mar 31 00:11:54 2015 +0200
    17.3 @@ -131,7 +131,7 @@
    17.4          val ((f, (_, f_defthm)), lthy') =
    17.5            Local_Theory.define
    17.6              ((Binding.name fname, mixfix),
    17.7 -              ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
    17.8 +              ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
    17.9                Term.subst_bound (fsum, f_def))) lthy
   17.10        in
   17.11          (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
    18.1 --- a/src/HOL/Tools/Function/partial_function.ML	Mon Mar 30 22:34:59 2015 +0200
    18.2 +++ b/src/HOL/Tools/Function/partial_function.ML	Tue Mar 31 00:11:54 2015 +0200
    18.3 @@ -262,7 +262,7 @@
    18.4      val inst_mono_thm = Thm.forall_elim (cert x_uc) mono_thm
    18.5  
    18.6      val f_def_rhs = curry_n arity (apply_inst lthy fixp F_uc);
    18.7 -    val f_def_binding = Binding.conceal (Binding.name (Thm.def_name fname));
    18.8 +    val f_def_binding = Binding.concealed (Binding.name (Thm.def_name fname));
    18.9      val ((f, (_, f_def)), lthy') = Local_Theory.define
   18.10        ((f_binding, mixfix), ((f_def_binding, []), f_def_rhs)) lthy;
   18.11  
    19.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Mon Mar 30 22:34:59 2015 +0200
    19.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Tue Mar 31 00:11:54 2015 +0200
    19.3 @@ -172,7 +172,7 @@
    19.4  
    19.5      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
    19.6        thy1
    19.7 -      |> Sign.map_naming Name_Space.conceal
    19.8 +      |> Sign.map_naming Name_Space.concealed
    19.9        |> Inductive.add_inductive_global
   19.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
   19.11             coind = false, no_elim = true, no_ind = false, skip_mono = true}
    20.1 --- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Mon Mar 30 22:34:59 2015 +0200
    20.2 +++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Tue Mar 31 00:11:54 2015 +0200
    20.3 @@ -201,7 +201,7 @@
    20.4      val raw_rhs = fold_rev (fn T => fn t => Abs ("", T, t)) (map snd ls @ [dummyT])
    20.5        (list_comb (Const (rec_name, dummyT), fs @ map Bound (0 :: (length ls downto 1))))
    20.6      val rhs = singleton (Syntax.check_terms ctxt) (Type.constraint varT raw_rhs);
    20.7 -  in (var, ((Binding.conceal (Binding.name def_name), []), rhs)) end;
    20.8 +  in (var, ((Binding.concealed (Binding.name def_name), []), rhs)) end;
    20.9  
   20.10  
   20.11  (* find datatypes which contain all datatypes in tnames' *)
    21.1 --- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Mon Mar 30 22:34:59 2015 +0200
    21.2 +++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Tue Mar 31 00:11:54 2015 +0200
    21.3 @@ -146,7 +146,7 @@
    21.4  
    21.5      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
    21.6        thy0
    21.7 -      |> Sign.map_naming Name_Space.conceal
    21.8 +      |> Sign.map_naming Name_Space.concealed
    21.9        |> Inductive.add_inductive_global
   21.10            {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
   21.11              coind = false, no_elim = false, no_ind = true, skip_mono = true}
    22.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Mon Mar 30 22:34:59 2015 +0200
    22.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Tue Mar 31 00:11:54 2015 +0200
    22.3 @@ -362,9 +362,9 @@
    22.4        val eqs_t = mk_equations (map2 (fn name => fn T => Free (name, T)) names Ts)
    22.5      in
    22.6        Function.add_function
    22.7 -        (map (fn (name, T) => (Binding.conceal (Binding.name name), SOME T, NoSyn))
    22.8 +        (map (fn (name, T) => (Binding.concealed (Binding.name name), SOME T, NoSyn))
    22.9            (names ~~ Ts))
   22.10 -        (map (pair (apfst Binding.conceal Attrib.empty_binding)) eqs_t)
   22.11 +        (map (pair (apfst Binding.concealed Attrib.empty_binding)) eqs_t)
   22.12          Function_Common.default_config pat_completeness_auto
   22.13        #> snd
   22.14        #> (fn lthy => Function.prove_termination NONE (the termination_tac lthy) lthy)
   22.15 @@ -372,8 +372,8 @@
   22.16      end
   22.17    else
   22.18      fold_map (fn (name, T) => Local_Theory.define
   22.19 -        ((Binding.conceal (Binding.name name), NoSyn),
   22.20 -          (apfst Binding.conceal Attrib.empty_binding, mk_undefined T))
   22.21 +        ((Binding.concealed (Binding.name name), NoSyn),
   22.22 +          (apfst Binding.concealed Attrib.empty_binding, mk_undefined T))
   22.23        #> apfst fst) (names ~~ Ts)
   22.24      #> (fn (consts, lthy) =>
   22.25        let
    23.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Mar 30 22:34:59 2015 +0200
    23.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Tue Mar 31 00:11:54 2015 +0200
    23.3 @@ -97,7 +97,7 @@
    23.4      val eqs1 = map (Pattern.rewrite_term thy rew_ts []) eqs0;
    23.5      val ((_, (_, eqs2)), lthy') = lthy
    23.6        |> BNF_LFP_Compat.add_primrec_simple
    23.7 -        [((Binding.conceal (Binding.name random_aux), T), NoSyn)] eqs1;
    23.8 +        [((Binding.concealed (Binding.name random_aux), T), NoSyn)] eqs1;
    23.9      val cT_random_aux = inst pt_random_aux;
   23.10      val cT_rhs = inst pt_rhs;
   23.11      val rule = @{thm random_aux_rec}
   23.12 @@ -136,8 +136,8 @@
   23.13          val projs = mk_proj (aux_lhs) Ts;
   23.14          val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs;
   23.15          val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) =>
   23.16 -          ((Binding.conceal (Binding.name name), NoSyn),
   23.17 -            (apfst Binding.conceal Attrib.empty_binding, rhs))) vs proj_eqs;
   23.18 +          ((Binding.concealed (Binding.name name), NoSyn),
   23.19 +            (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs;
   23.20          val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq;
   23.21          fun prove_eqs aux_simp proj_defs lthy = 
   23.22            let
   23.23 @@ -168,7 +168,7 @@
   23.24          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
   23.25          val tac = ALLGOALS (Proof_Context.fact_tac lthy ext_simps);
   23.26        in (map (fn prop => Goal.prove_sorry lthy vs [] prop (K tac)) eqs, lthy) end;
   23.27 -    val b = Binding.conceal (Binding.qualify true prfx
   23.28 +    val b = Binding.concealed (Binding.qualify true prfx
   23.29        (Binding.qualify true name (Binding.name "simps")));
   23.30    in
   23.31      lthy
   23.32 @@ -262,7 +262,7 @@
   23.33      |> random_aux_specification prfx random_auxN auxs_eqs
   23.34      |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
   23.35      |-> (fn random_defs' => fold_map (fn random_def =>
   23.36 -          Specification.definition (NONE, (apfst Binding.conceal
   23.37 +          Specification.definition (NONE, (apfst Binding.concealed
   23.38              Attrib.empty_binding, random_def))) random_defs')
   23.39      |> snd
   23.40      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
    24.1 --- a/src/HOL/Tools/inductive.ML	Mon Mar 30 22:34:59 2015 +0200
    24.2 +++ b/src/HOL/Tools/inductive.ML	Tue Mar 31 00:11:54 2015 +0200
    24.3 @@ -843,10 +843,10 @@
    24.4  
    24.5      val is_auxiliary = length cs >= 2; 
    24.6      val ((rec_const, (_, fp_def)), lthy') = lthy
    24.7 -      |> is_auxiliary ? Local_Theory.conceal
    24.8 +      |> is_auxiliary ? Local_Theory.concealed
    24.9        |> Local_Theory.define
   24.10          ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
   24.11 -         ((Binding.conceal (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
   24.12 +         ((Binding.concealed (Thm.def_binding rec_name), @{attributes [nitpick_unfold]}),
   24.13             fold_rev lambda params
   24.14               (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
   24.15        ||> is_auxiliary ? Local_Theory.restore_naming lthy;
   24.16 @@ -862,7 +862,7 @@
   24.17              val xs =
   24.18                map Free (Variable.variant_frees lthy intr_ts (mk_names "x" (length Ts) ~~ Ts));
   24.19            in
   24.20 -            (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
   24.21 +            (name_mx, (apfst Binding.concealed Attrib.empty_binding, fold_rev lambda (params @ xs)
   24.22                (list_comb (rec_const, params @ make_bool_args' bs i @
   24.23                  make_args argTs (xs ~~ Ts)))))
   24.24            end) (cnames_syn ~~ cs);
   24.25 @@ -873,7 +873,7 @@
   24.26      val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';
   24.27      val mono = prove_mono quiet_mode skip_mono predT fp_fun monos lthy''';
   24.28      val (_, lthy'''') =
   24.29 -      Local_Theory.note (apfst Binding.conceal Attrib.empty_binding,
   24.30 +      Local_Theory.note (apfst Binding.concealed Attrib.empty_binding,
   24.31          Proof_Context.export lthy''' lthy'' [mono]) lthy'';
   24.32  
   24.33    in (lthy'''', lthy''', rec_name, mono, fp_def', map (#2 o #2) consts_defs,
    25.1 --- a/src/HOL/Tools/inductive_set.ML	Mon Mar 30 22:34:59 2015 +0200
    25.2 +++ b/src/HOL/Tools/inductive_set.ML	Tue Mar 31 00:11:54 2015 +0200
    25.3 @@ -488,7 +488,7 @@
    25.4  
    25.5      (* define inductive sets using previously defined predicates *)
    25.6      val (defs, lthy2) = lthy1
    25.7 -      |> Local_Theory.conceal  (* FIXME ?? *)
    25.8 +      |> Local_Theory.concealed  (* FIXME ?? *)
    25.9        |> fold_map Local_Theory.define
   25.10          (map (fn (((c, syn), (fs, U, _)), p) => ((c, syn), ((Thm.def_binding c, []),
   25.11             fold_rev lambda params (HOLogic.Collect_const U $
    26.1 --- a/src/HOL/Tools/recdef.ML	Mon Mar 30 22:34:59 2015 +0200
    26.2 +++ b/src/HOL/Tools/recdef.ML	Tue Mar 31 00:11:54 2015 +0200
    26.3 @@ -260,7 +260,7 @@
    26.4          " in recdef definition of " ^ quote name);
    26.5    in
    26.6      Specification.theorem "" NONE (K I)
    26.7 -      (Binding.conceal (Binding.name bname), atts) [] []
    26.8 +      (Binding.concealed (Binding.name bname), atts) [] []
    26.9        (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   26.10    end;
   26.11  
    27.1 --- a/src/HOL/Tools/record.ML	Mon Mar 30 22:34:59 2015 +0200
    27.2 +++ b/src/HOL/Tools/record.ML	Tue Mar 31 00:11:54 2015 +0200
    27.3 @@ -152,7 +152,7 @@
    27.4        typ_thy
    27.5        |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
    27.6        |> Global_Theory.add_defs false
    27.7 -        [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
    27.8 +        [((Binding.concealed (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
    27.9  
   27.10      val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
   27.11      val cons = Const (@{const_name Record.iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
   27.12 @@ -1720,7 +1720,7 @@
   27.13      thy
   27.14      |> Class.instantiation ([tyco], vs, sort)
   27.15      |> `(fn lthy => Syntax.check_term lthy eq)
   27.16 -    |-> (fn eq => Specification.definition (NONE, (apfst Binding.conceal Attrib.empty_binding, eq)))
   27.17 +    |-> (fn eq => Specification.definition (NONE, (apfst Binding.concealed Attrib.empty_binding, eq)))
   27.18      |> snd
   27.19      |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   27.20    end;
   27.21 @@ -2017,12 +2017,12 @@
   27.22            |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
   27.23              (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   27.24            |> (Global_Theory.add_defs false o
   27.25 -                map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
   27.26 +                map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) sel_specs
   27.27            ||>> (Global_Theory.add_defs false o
   27.28 -                map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
   27.29 +                map (Thm.no_attributes o apfst (Binding.concealed o Binding.name))) upd_specs
   27.30            ||>> (Global_Theory.add_defs false o
   27.31                  map (rpair [Code.add_default_eqn_attribute]
   27.32 -                o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
   27.33 +                o apfst (Binding.concealed o Binding.name))) (*FIXME Spec_Rules (?)*)
   27.34              [make_spec, fields_spec, extend_spec, truncate_spec]);
   27.35      val defs_ctxt = Proof_Context.init_global defs_thy;
   27.36  
    28.1 --- a/src/HOL/Tools/typedef.ML	Mon Mar 30 22:34:59 2015 +0200
    28.2 +++ b/src/HOL/Tools/typedef.ML	Tue Mar 31 00:11:54 2015 +0200
    28.3 @@ -137,9 +137,9 @@
    28.4  
    28.5  (* prepare_typedef *)
    28.6  
    28.7 -fun prepare_typedef conceal prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
    28.8 +fun prepare_typedef concealed prep_term (name, raw_args, mx) raw_set opt_morphs lthy =
    28.9    let
   28.10 -    val concealed_name = name |> conceal ? Binding.conceal;
   28.11 +    val concealed_name = name |> concealed ? Binding.concealed;
   28.12      val bname = Binding.name_of name;
   28.13  
   28.14  
   28.15 @@ -242,18 +242,18 @@
   28.16  
   28.17  (* add_typedef: tactic interface *)
   28.18  
   28.19 -fun add_typedef conceal typ set opt_morphs tac lthy =
   28.20 +fun add_typedef concealed typ set opt_morphs tac lthy =
   28.21    let
   28.22      val ((goal, _, typedef_result), lthy') =
   28.23 -      prepare_typedef conceal Syntax.check_term typ set opt_morphs lthy;
   28.24 +      prepare_typedef concealed Syntax.check_term typ set opt_morphs lthy;
   28.25      val inhabited =
   28.26        Goal.prove lthy' [] [] goal (tac o #context)
   28.27        |> Goal.norm_result lthy' |> Thm.close_derivation;
   28.28    in typedef_result inhabited lthy' end;
   28.29  
   28.30 -fun add_typedef_global conceal typ set opt_morphs tac =
   28.31 +fun add_typedef_global concealed typ set opt_morphs tac =
   28.32    Named_Target.theory_init
   28.33 -  #> add_typedef conceal typ set opt_morphs tac
   28.34 +  #> add_typedef concealed typ set opt_morphs tac
   28.35    #> Local_Theory.exit_result_global (apsnd o transform_info);
   28.36  
   28.37  
    29.1 --- a/src/Pure/General/binding.ML	Mon Mar 30 22:34:59 2015 +0200
    29.2 +++ b/src/Pure/General/binding.ML	Tue Mar 31 00:11:54 2015 +0200
    29.3 @@ -10,7 +10,7 @@
    29.4  signature BINDING =
    29.5  sig
    29.6    eqtype binding
    29.7 -  val dest: binding -> {private: bool, conceal: bool, path: (string * bool) list, name: bstring}
    29.8 +  val dest: binding -> {private: bool, concealed: bool, path: (string * bool) list, name: bstring}
    29.9    val path_of: binding -> (string * bool) list
   29.10    val make: bstring * Position.T -> binding
   29.11    val pos_of: binding -> Position.T
   29.12 @@ -30,7 +30,7 @@
   29.13    val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
   29.14    val prefix: bool -> string -> binding -> binding
   29.15    val private: binding -> binding
   29.16 -  val conceal: binding -> binding
   29.17 +  val concealed: binding -> binding
   29.18    val pretty: binding -> Pretty.T
   29.19    val print: binding -> string
   29.20    val pp: binding -> Pretty.T
   29.21 @@ -47,21 +47,21 @@
   29.22  
   29.23  datatype binding = Binding of
   29.24   {private: bool,                    (*entry is strictly private -- no name space accesses*)
   29.25 -  conceal: bool,                    (*entry is for foundational purposes -- please ignore*)
   29.26 +  concealed: bool,                  (*entry is for foundational purposes -- please ignore*)
   29.27    prefix: (string * bool) list,     (*system prefix*)
   29.28    qualifier: (string * bool) list,  (*user qualifier*)
   29.29    name: bstring,                    (*base name*)
   29.30    pos: Position.T};                 (*source position*)
   29.31  
   29.32 -fun make_binding (private, conceal, prefix, qualifier, name, pos) =
   29.33 -  Binding {private = private, conceal = conceal, prefix = prefix,
   29.34 +fun make_binding (private, concealed, prefix, qualifier, name, pos) =
   29.35 +  Binding {private = private, concealed = concealed, prefix = prefix,
   29.36      qualifier = qualifier, name = name, pos = pos};
   29.37  
   29.38 -fun map_binding f (Binding {private, conceal, prefix, qualifier, name, pos}) =
   29.39 -  make_binding (f (private, conceal, prefix, qualifier, name, pos));
   29.40 +fun map_binding f (Binding {private, concealed, prefix, qualifier, name, pos}) =
   29.41 +  make_binding (f (private, concealed, prefix, qualifier, name, pos));
   29.42  
   29.43 -fun dest (Binding {private, conceal, prefix, qualifier, name, ...}) =
   29.44 -  {private = private, conceal = conceal, path = prefix @ qualifier, name = name};
   29.45 +fun dest (Binding {private, concealed, prefix, qualifier, name, ...}) =
   29.46 +  {private = private, concealed = concealed, path = prefix @ qualifier, name = name};
   29.47  
   29.48  val path_of = #path o dest;
   29.49  
   29.50 @@ -75,8 +75,8 @@
   29.51  
   29.52  fun pos_of (Binding {pos, ...}) = pos;
   29.53  fun set_pos pos =
   29.54 -  map_binding (fn (private, conceal, prefix, qualifier, name, _) =>
   29.55 -    (private, conceal, prefix, qualifier, name, pos));
   29.56 +  map_binding (fn (private, concealed, prefix, qualifier, name, _) =>
   29.57 +    (private, concealed, prefix, qualifier, name, pos));
   29.58  
   29.59  fun name name = make (name, Position.none);
   29.60  fun name_of (Binding {name, ...}) = name;
   29.61 @@ -84,8 +84,8 @@
   29.62  fun eq_name (b, b') = name_of b = name_of b';
   29.63  
   29.64  fun map_name f =
   29.65 -  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
   29.66 -    (private, conceal, prefix, qualifier, f name, pos));
   29.67 +  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   29.68 +    (private, concealed, prefix, qualifier, f name, pos));
   29.69  
   29.70  val prefix_name = map_name o prefix;
   29.71  val suffix_name = map_name o suffix;
   29.72 @@ -98,13 +98,13 @@
   29.73  
   29.74  fun qualify _ "" = I
   29.75    | qualify mandatory qual =
   29.76 -      map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
   29.77 -        (private, conceal, prefix, (qual, mandatory) :: qualifier, name, pos));
   29.78 +      map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   29.79 +        (private, concealed, prefix, (qual, mandatory) :: qualifier, name, pos));
   29.80  
   29.81  fun qualified mandatory name' =
   29.82 -  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
   29.83 +  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   29.84      let val qualifier' = if name = "" then qualifier else qualifier @ [(name, mandatory)]
   29.85 -    in (private, conceal, prefix, qualifier', name', pos) end);
   29.86 +    in (private, concealed, prefix, qualifier', name', pos) end);
   29.87  
   29.88  fun qualified_name "" = empty
   29.89    | qualified_name s =
   29.90 @@ -117,8 +117,8 @@
   29.91  fun prefix_of (Binding {prefix, ...}) = prefix;
   29.92  
   29.93  fun map_prefix f =
   29.94 -  map_binding (fn (private, conceal, prefix, qualifier, name, pos) =>
   29.95 -    (private, conceal, f prefix, qualifier, name, pos));
   29.96 +  map_binding (fn (private, concealed, prefix, qualifier, name, pos) =>
   29.97 +    (private, concealed, f prefix, qualifier, name, pos));
   29.98  
   29.99  fun prefix _ "" = I
  29.100    | prefix mandatory prfx = map_prefix (cons (prfx, mandatory));
  29.101 @@ -127,10 +127,10 @@
  29.102  (* visibility flags *)
  29.103  
  29.104  val private =
  29.105 -  map_binding (fn (_, conceal, prefix, qualifier, name, pos) =>
  29.106 -    (true, conceal, prefix, qualifier, name, pos));
  29.107 +  map_binding (fn (_, concealed, prefix, qualifier, name, pos) =>
  29.108 +    (true, concealed, prefix, qualifier, name, pos));
  29.109  
  29.110 -val conceal =
  29.111 +val concealed =
  29.112    map_binding (fn (private, _, prefix, qualifier, name, pos) =>
  29.113      (private, true, prefix, qualifier, name, pos));
  29.114  
    30.1 --- a/src/Pure/General/name_space.ML	Mon Mar 30 22:34:59 2015 +0200
    30.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 31 00:11:54 2015 +0200
    30.3 @@ -34,7 +34,7 @@
    30.4    val merge: T * T -> T
    30.5    type naming
    30.6    val private: naming -> naming
    30.7 -  val conceal: naming -> naming
    30.8 +  val concealed: naming -> naming
    30.9    val get_group: naming -> serial option
   30.10    val set_group: serial option -> naming -> naming
   30.11    val set_theory_name: string -> naming -> naming
   30.12 @@ -285,36 +285,36 @@
   30.13  
   30.14  datatype naming = Naming of
   30.15   {private: bool,
   30.16 -  conceal: bool,
   30.17 +  concealed: bool,
   30.18    group: serial option,
   30.19    theory_name: string,
   30.20    path: (string * bool) list};
   30.21  
   30.22 -fun make_naming (private, conceal, group, theory_name, path) =
   30.23 -  Naming {private = private, conceal = conceal, group = group,
   30.24 +fun make_naming (private, concealed, group, theory_name, path) =
   30.25 +  Naming {private = private, concealed = concealed, group = group,
   30.26      theory_name = theory_name, path = path};
   30.27  
   30.28 -fun map_naming f (Naming {private, conceal, group, theory_name, path}) =
   30.29 -  make_naming (f (private, conceal, group, theory_name, path));
   30.30 +fun map_naming f (Naming {private, concealed, group, theory_name, path}) =
   30.31 +  make_naming (f (private, concealed, group, theory_name, path));
   30.32  
   30.33 -fun map_path f = map_naming (fn (private, conceal, group, theory_name, path) =>
   30.34 -  (private, conceal, group, theory_name, f path));
   30.35 +fun map_path f = map_naming (fn (private, concealed, group, theory_name, path) =>
   30.36 +  (private, concealed, group, theory_name, f path));
   30.37  
   30.38  
   30.39 -val private = map_naming (fn (_, conceal, group, theory_name, path) =>
   30.40 -  (true, conceal, group, theory_name, path));
   30.41 +val private = map_naming (fn (_, concealed, group, theory_name, path) =>
   30.42 +  (true, concealed, group, theory_name, path));
   30.43  
   30.44 -val conceal = map_naming (fn (private, _, group, theory_name, path) =>
   30.45 +val concealed = map_naming (fn (private, _, group, theory_name, path) =>
   30.46    (private, true, group, theory_name, path));
   30.47  
   30.48 -fun set_theory_name theory_name = map_naming (fn (private, conceal, group, _, path) =>
   30.49 -  (private, conceal, group, theory_name, path));
   30.50 +fun set_theory_name theory_name = map_naming (fn (private, concealed, group, _, path) =>
   30.51 +  (private, concealed, group, theory_name, path));
   30.52  
   30.53  
   30.54  fun get_group (Naming {group, ...}) = group;
   30.55  
   30.56 -fun set_group group = map_naming (fn (private, conceal, _, theory_name, path) =>
   30.57 -  (private, conceal, group, theory_name, path));
   30.58 +fun set_group group = map_naming (fn (private, concealed, _, theory_name, path) =>
   30.59 +  (private, concealed, group, theory_name, path));
   30.60  
   30.61  fun new_group naming = set_group (SOME (serial ())) naming;
   30.62  val reset_group = set_group NONE;
   30.63 @@ -335,16 +335,16 @@
   30.64  
   30.65  fun err_bad binding = error (Binding.bad binding);
   30.66  
   30.67 -fun transform_binding (Naming {private, conceal, ...}) =
   30.68 +fun transform_binding (Naming {private, concealed, ...}) =
   30.69    private ? Binding.private #>
   30.70 -  conceal ? Binding.conceal;
   30.71 +  concealed ? Binding.concealed;
   30.72  
   30.73  val bad_specs = ["", "??", "__"];
   30.74  
   30.75  fun name_spec (naming as Naming {path = path1, ...}) raw_binding =
   30.76    let
   30.77      val binding = transform_binding naming raw_binding;
   30.78 -    val {private, conceal, path = path2, name} = Binding.dest binding;
   30.79 +    val {private, concealed, path = path2, name} = Binding.dest binding;
   30.80      val _ = Long_Name.is_qualified name andalso err_bad binding;
   30.81  
   30.82      val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path1 @ path2);
   30.83 @@ -353,7 +353,7 @@
   30.84      val _ =
   30.85        exists (fn (a, _) => member (op =) bad_specs a orelse exists_string (fn s => s = "\"") a) spec
   30.86        andalso err_bad binding;
   30.87 -  in {private = private, conceal = conceal, spec = if null spec2 then [] else spec} end;
   30.88 +  in {private = private, concealed = concealed, spec = if null spec2 then [] else spec} end;
   30.89  
   30.90  fun full_name naming =
   30.91    name_spec naming #> #spec #> map #1 #> Long_Name.implode;
   30.92 @@ -442,7 +442,7 @@
   30.93    let
   30.94      val naming = naming_of context;
   30.95      val Naming {group, theory_name, ...} = naming;
   30.96 -    val {conceal, spec, ...} = name_spec naming binding;
   30.97 +    val {concealed, spec, ...} = name_spec naming binding;
   30.98      val (accs, accs') = accesses naming binding;
   30.99  
  30.100      val name = Long_Name.implode (map fst spec);
  30.101 @@ -450,7 +450,7 @@
  30.102  
  30.103      val (proper_pos, pos) = Position.default (Binding.pos_of binding);
  30.104      val entry =
  30.105 -     {concealed = conceal,
  30.106 +     {concealed = concealed,
  30.107        group = group,
  30.108        theory_name = theory_name,
  30.109        pos = pos,
    31.1 --- a/src/Pure/Isar/expression.ML	Mon Mar 30 22:34:59 2015 +0200
    31.2 +++ b/src/Pure/Isar/expression.ML	Tue Mar 31 00:11:54 2015 +0200
    31.3 @@ -674,9 +674,9 @@
    31.4      val ([pred_def], defs_thy) =
    31.5        thy
    31.6        |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name]
    31.7 -      |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
    31.8 +      |> Sign.declare_const_global ((Binding.concealed binding, predT), NoSyn) |> snd
    31.9        |> Global_Theory.add_defs false
   31.10 -        [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   31.11 +        [((Binding.concealed (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   31.12      val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
   31.13  
   31.14      val intro = Goal.prove_global defs_thy [] norm_ts statement
   31.15 @@ -721,7 +721,7 @@
   31.16              thy'
   31.17              |> Sign.qualified_path true abinding
   31.18              |> Global_Theory.note_thmss ""
   31.19 -              [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
   31.20 +              [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
   31.21              ||> Sign.restore_naming thy';
   31.22            in (SOME statement, SOME intro, axioms, thy'') end;
   31.23      val (b_pred, b_intro, b_axioms, thy'''') =
   31.24 @@ -736,8 +736,8 @@
   31.25              thy'''
   31.26              |> Sign.qualified_path true binding
   31.27              |> Global_Theory.note_thmss ""
   31.28 -                 [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   31.29 -                  ((Binding.conceal (Binding.name axiomsN), []),
   31.30 +                 [((Binding.concealed (Binding.name introN), []), [([intro], [Locale.intro_add])]),
   31.31 +                  ((Binding.concealed (Binding.name axiomsN), []),
   31.32                      [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms,
   31.33                        [])])]
   31.34              ||> Sign.restore_naming thy''';
   31.35 @@ -806,7 +806,7 @@
   31.36  
   31.37      val notes =
   31.38        if is_some asm then
   31.39 -        [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   31.40 +        [("", [((Binding.concealed (Binding.suffix_name ("_" ^ axiomsN) binding), []),
   31.41            [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))],
   31.42              [(Attrib.internal o K) Locale.witness_add])])])]
   31.43        else [];
    32.1 --- a/src/Pure/Isar/local_theory.ML	Mon Mar 30 22:34:59 2015 +0200
    32.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Mar 31 00:11:54 2015 +0200
    32.3 @@ -28,7 +28,7 @@
    32.4    val naming_of: local_theory -> Name_Space.naming
    32.5    val full_name: local_theory -> binding -> string
    32.6    val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
    32.7 -  val conceal: local_theory -> local_theory
    32.8 +  val concealed: local_theory -> local_theory
    32.9    val new_group: local_theory -> local_theory
   32.10    val reset_group: local_theory -> local_theory
   32.11    val restore_naming: local_theory -> local_theory -> local_theory
   32.12 @@ -188,7 +188,7 @@
   32.13    map_top (fn (naming, operations, after_close, brittle, target) =>
   32.14      (f naming, operations, after_close, brittle, target));
   32.15  
   32.16 -val conceal = map_naming Name_Space.conceal;
   32.17 +val concealed = map_naming Name_Space.concealed;
   32.18  val new_group = map_naming Name_Space.new_group;
   32.19  val reset_group = map_naming Name_Space.reset_group;
   32.20  
    33.1 --- a/src/Pure/Isar/locale.ML	Mon Mar 30 22:34:59 2015 +0200
    33.2 +++ b/src/Pure/Isar/locale.ML	Tue Mar 31 00:11:54 2015 +0200
    33.3 @@ -592,7 +592,7 @@
    33.4  
    33.5  fun add_decl loc decl =
    33.6    add_thmss loc ""
    33.7 -    [((Binding.conceal Binding.empty,
    33.8 +    [((Binding.concealed Binding.empty,
    33.9          [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
   33.10        [([Drule.dummy_thm], [])])];
   33.11  
    34.1 --- a/src/Pure/Isar/proof_context.ML	Mon Mar 30 22:34:59 2015 +0200
    34.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 31 00:11:54 2015 +0200
    34.3 @@ -1195,7 +1195,7 @@
    34.4        (Name_Space.del_table name cases, index)
    34.5    | update_case context is_proper (name, SOME c) (cases, index) =
    34.6        let
    34.7 -        val binding = Binding.name name |> not is_proper ? Binding.conceal;
    34.8 +        val binding = Binding.name name |> not is_proper ? Binding.concealed;
    34.9          val (_, cases') = Name_Space.define context false (binding, ((c, is_proper), index)) cases;
   34.10          val index' = index + 1;
   34.11        in (cases', index') end;
    35.1 --- a/src/Pure/axclass.ML	Mon Mar 30 22:34:59 2015 +0200
    35.2 +++ b/src/Pure/axclass.ML	Tue Mar 31 00:11:54 2015 +0200
    35.3 @@ -362,7 +362,7 @@
    35.4          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
    35.5        #>> apsnd Thm.varifyT_global
    35.6        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
    35.7 -        #> Global_Theory.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    35.8 +        #> Global_Theory.add_thm ((Binding.concealed (Binding.name c'), thm), [])
    35.9          #> #2
   35.10          #> pair (Const (c, T))))
   35.11      ||> Sign.restore_naming thy
   35.12 @@ -392,7 +392,7 @@
   35.13      val rel = Logic.dest_classrel prop handle TERM _ => err ();
   35.14      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
   35.15      val binding =
   35.16 -      Binding.conceal (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
   35.17 +      Binding.concealed (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))));
   35.18      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   35.19      val th'' = th'
   35.20        |> Thm.unconstrainT
   35.21 @@ -413,7 +413,7 @@
   35.22      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
   35.23  
   35.24      val binding =
   35.25 -      Binding.conceal (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
   35.26 +      Binding.concealed (Binding.name (prefix arity_prefix (Logic.name_arity arity)));
   35.27      val (th', thy') = Global_Theory.store_thm (binding, th) thy;
   35.28  
   35.29      val args = Name.invent_names Name.context Name.aT Ss;
    36.1 --- a/src/Pure/drule.ML	Mon Mar 30 22:34:59 2015 +0200
    36.2 +++ b/src/Pure/drule.ML	Tue Mar 31 00:11:54 2015 +0200
    36.3 @@ -599,11 +599,11 @@
    36.4  val protect = Thm.apply (certify Logic.protectC);
    36.5  
    36.6  val protectI =
    36.7 -  store_standard_thm (Binding.conceal (Binding.make ("protectI", @{here})))
    36.8 +  store_standard_thm (Binding.concealed (Binding.make ("protectI", @{here})))
    36.9      (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
   36.10  
   36.11  val protectD =
   36.12 -  store_standard_thm (Binding.conceal (Binding.make ("protectD", @{here})))
   36.13 +  store_standard_thm (Binding.concealed (Binding.make ("protectD", @{here})))
   36.14      (Thm.equal_elim prop_def (Thm.assume (protect A)));
   36.15  
   36.16  val protect_cong =
   36.17 @@ -622,7 +622,7 @@
   36.18  (* term *)
   36.19  
   36.20  val termI =
   36.21 -  store_standard_thm (Binding.conceal (Binding.make ("termI", @{here})))
   36.22 +  store_standard_thm (Binding.concealed (Binding.make ("termI", @{here})))
   36.23      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
   36.24  
   36.25  fun mk_term ct =
   36.26 @@ -648,11 +648,11 @@
   36.27  (* sort_constraint *)
   36.28  
   36.29  val sort_constraintI =
   36.30 -  store_standard_thm (Binding.conceal (Binding.make ("sort_constraintI", @{here})))
   36.31 +  store_standard_thm (Binding.concealed (Binding.make ("sort_constraintI", @{here})))
   36.32      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
   36.33  
   36.34  val sort_constraint_eq =
   36.35 -  store_standard_thm (Binding.conceal (Binding.make ("sort_constraint_eq", @{here})))
   36.36 +  store_standard_thm (Binding.concealed (Binding.make ("sort_constraint_eq", @{here})))
   36.37      (Thm.equal_intr
   36.38        (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
   36.39          (Thm.unvarify_global sort_constraintI)))