--- a/src/HOL/Nominal/nominal_datatype.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 28 16:25:27 2009 +0100
@@ -567,13 +567,16 @@
val rep_set_names'' = map (Sign.full_bname thy3) rep_set_names';
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
- Inductive.add_inductive_global (serial ())
+ thy3
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
(rep_set_names' ~~ recTs'))
- [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy3;
+ [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ ||> Sign.restore_naming thy3;
(**** Prove that representing set is closed under permutation ****)
@@ -1508,15 +1511,17 @@
([], [], [], [], 0);
val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
- thy10 |>
- Inductive.add_inductive_global (serial ())
+ thy10
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] ||>
- PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct");
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ ||> PureThy.hide_fact true (Long_Name.append (Sign.full_bname thy10 big_rec_name) "induct")
+ ||> Sign.restore_naming thy10;
(** equivariance **)
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Wed Oct 28 16:25:27 2009 +0100
@@ -153,13 +153,17 @@
(descr' ~~ recTs ~~ rec_sets') ([], 0);
val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
- Inductive.add_inductive_global (serial ())
+ thy0
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
(map dest_Free rec_fns)
- (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0;
+ (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []
+ ||> Sign.restore_naming thy0
+ ||> Theory.checkpoint;
(* prove uniqueness and termination of primrec combinators *)
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Wed Oct 28 16:25:27 2009 +0100
@@ -170,12 +170,16 @@
((1 upto (length constrs)) ~~ constrs)) (descr' ~~ rep_set_names');
val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
- Inductive.add_inductive_global (serial ())
+ thy1
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
- (map (fn x => (Attrib.empty_binding, x)) intr_ts) [] thy1;
+ (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
+ ||> Sign.restore_naming thy1
+ ||> Theory.checkpoint;
(********************************* typedef ********************************)
--- a/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Function/function_core.ML Wed Oct 28 16:25:27 2009 +0100
@@ -488,7 +488,9 @@
|> Syntax.check_term lthy
val ((f, (_, f_defthm)), lthy) =
- LocalTheory.define Thm.internalK ((Binding.name (function_name fname), mixfix), ((Binding.name fdefname, []), f_def)) lthy
+ LocalTheory.define Thm.internalK
+ ((Binding.name (function_name fname), mixfix),
+ ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
in
((f, f_defthm), lthy)
end
--- a/src/HOL/Tools/Function/inductive_wrap.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Function/inductive_wrap.ML Wed Oct 28 16:25:27 2009 +0100
@@ -39,7 +39,9 @@
fun inductive_def defs (((R, T), mixfix), lthy) =
let
val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
- Inductive.add_inductive_i
+ lthy
+ |> LocalTheory.conceal
+ |> Inductive.add_inductive_i
{quiet_mode = false,
verbose = ! Toplevel.debug,
kind = Thm.internalK,
@@ -53,7 +55,7 @@
[] (* no parameters *)
(map (fn t => (Attrib.empty_binding, t)) defs) (* the intros *)
[] (* no special monos *)
- lthy
+ ||> LocalTheory.restore_naming lthy
val intrs = map2 (requantify lthy (R, T)) defs intrs_gen
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Oct 28 16:25:27 2009 +0100
@@ -368,14 +368,18 @@
if is_some (try (map (cterm_of thy)) intr_ts) then
let
val (ind_result, thy') =
- Inductive.add_inductive_global (serial ())
+ thy
+ |> Sign.map_naming Name_Space.conceal
+ |> Inductive.add_inductive_global (serial ())
{quiet_mode = false, verbose = false, kind = Thm.internalK,
alt_name = Binding.empty, coind = false, no_elim = false,
no_ind = false, skip_mono = false, fork_mono = false}
- (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
+ (map (fn (s, T) =>
+ ((Binding.name s, T), NoSyn)) (distinct (op =) (map dest_Free preds)))
pnames
(map (fn x => (Attrib.empty_binding, x)) intr_ts)
- [] thy
+ []
+ ||> Sign.restore_naming thy
val prednames = map (fst o dest_Const) (#preds ind_result)
(* val rewr_thms = map mk_rewr_eq ((distinct (op =) funs) ~~ (#preds ind_result)) *)
(* add constants to my table *)
--- a/src/HOL/Tools/inductive.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/inductive.ML Wed Oct 28 16:25:27 2009 +0100
@@ -592,7 +592,7 @@
(** specification of (co)inductive predicates **)
fun mk_ind_def quiet_mode skip_mono fork_mono alt_name coind cs intr_ts monos params cnames_syn ctxt =
- let
+ let (* FIXME proper naming convention: lthy *)
val fp_name = if coind then @{const_name Inductive.gfp} else @{const_name Inductive.lfp};
val argTs = fold (combine (op =) o arg_types_of (length params)) cs [];
@@ -649,30 +649,37 @@
Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
else alt_name;
- val ((rec_const, (_, fp_def)), ctxt') = ctxt |>
- LocalTheory.define Thm.internalK
+ val ((rec_const, (_, fp_def)), ctxt') = ctxt
+ |> LocalTheory.conceal
+ |> LocalTheory.define Thm.internalK
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
(Attrib.empty_binding, fold_rev lambda params
- (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)));
+ (Const (fp_name, (predT --> predT) --> predT) $ fp_fun)))
+ ||> LocalTheory.restore_naming ctxt;
val fp_def' = Simplifier.rewrite (HOL_basic_ss addsimps [fp_def])
(cterm_of (ProofContext.theory_of ctxt') (list_comb (rec_const, params)));
- val specs = if length cs < 2 then [] else
- map_index (fn (i, (name_mx, c)) =>
- let
- val Ts = arg_types_of (length params) c;
- val xs = map Free (Variable.variant_frees ctxt intr_ts
- (mk_names "x" (length Ts) ~~ Ts))
- in
- (name_mx, (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);
- val (consts_defs, ctxt'') = fold_map (LocalTheory.define Thm.internalK) specs ctxt';
+ val specs =
+ if length cs < 2 then []
+ else
+ map_index (fn (i, (name_mx, c)) =>
+ let
+ val Ts = arg_types_of (length params) c;
+ val xs = map Free (Variable.variant_frees ctxt intr_ts
+ (mk_names "x" (length Ts) ~~ Ts))
+ in
+ (name_mx, (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);
+ val (consts_defs, ctxt'') = ctxt'
+ |> LocalTheory.conceal
+ |> fold_map (LocalTheory.define Thm.internalK) specs
+ ||> LocalTheory.restore_naming ctxt';
val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt'';
val ((_, [mono']), ctxt''') =
- LocalTheory.note Thm.internalK (Attrib.empty_binding, [mono]) ctxt'';
+ LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) ctxt'';
in (ctxt''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
@@ -697,7 +704,8 @@
val (intrs', ctxt1) =
ctxt |>
LocalTheory.notes kind
- (map (rec_qualified false) intr_bindings ~~ intr_atts ~~ map (fn th => [([th],
+ (map (rec_qualified false) intr_bindings ~~ intr_atts ~~
+ map (fn th => [([th],
[Attrib.internal (K (ContextRules.intro_query NONE)),
Attrib.internal (K Nitpick_Intros.add)])]) intrs) |>>
map (hd o snd);
--- a/src/HOL/Tools/inductive_set.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML Wed Oct 28 16:25:27 2009 +0100
@@ -407,7 +407,7 @@
fun add_ind_set_def
{quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
cs intros monos params cnames_syn ctxt =
- let
+ let (* FIXME proper naming convention: lthy *)
val thy = ProofContext.theory_of ctxt;
val {set_arities, pred_arities, to_pred_simps, ...} =
PredSetConvData.get (Context.Proof ctxt);
@@ -419,7 +419,8 @@
val new_arities = filter_out
(fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
| _ => false) (fold (snd #> infer) intros []);
- val params' = map (fn x => (case AList.lookup op = new_arities x of
+ val params' = map (fn x =>
+ (case AList.lookup op = new_arities x of
SOME fs =>
let
val T = HOLogic.dest_setT (fastype_of x);
@@ -482,11 +483,14 @@
cs' intros' monos' params1 cnames_syn' ctxt;
(* define inductive sets using previously defined predicates *)
- val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
- (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
- fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
- (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
+ val (defs, ctxt2) = ctxt1
+ |> LocalTheory.conceal (* FIXME ?? *)
+ |> fold_map (LocalTheory.define Thm.internalK)
+ (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
+ fold_rev lambda params (HOLogic.Collect_const U $
+ HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
+ (cnames_syn ~~ cs_info ~~ preds))
+ ||> LocalTheory.restore_naming ctxt1;
(* prove theorems for converting predicate to set notation *)
val ctxt3 = fold
--- a/src/HOL/Tools/recdef.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/HOL/Tools/recdef.ML Wed Oct 28 16:25:27 2009 +0100
@@ -263,8 +263,9 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
- [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+ Specification.theorem Thm.internalK NONE (K I)
+ (Binding.conceal (Binding.name bname), atts) []
+ (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
--- a/src/Pure/Isar/expression.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/Pure/Isar/expression.ML Wed Oct 28 16:25:27 2009 +0100
@@ -641,7 +641,8 @@
|> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
|> Sign.declare_const ((bname, predT), NoSyn) |> snd
|> PureThy.add_defs false
- [((Binding.map_name Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
+ [((Binding.conceal (Binding.map_name Thm.def_name bname), Logic.mk_equals (head, body)),
+ [Thm.kind_internal])];
val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
val cert = Thm.cterm_of defs_thy;
@@ -682,7 +683,7 @@
thy'
|> Sign.mandatory_path (Binding.name_of aname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.unfold_add])])]
+ [((Binding.conceal (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'''') =
@@ -696,8 +697,8 @@
thy'''
|> Sign.mandatory_path (Binding.name_of pname)
|> PureThy.note_thmss Thm.internalK
- [((Binding.name introN, []), [([intro], [Locale.intro_add])]),
- ((Binding.name axiomsN, []),
+ [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
+ ((Binding.conceal (Binding.name axiomsN), []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
||> Sign.restore_naming thy''';
in (SOME statement, SOME intro, axioms, thy'''') end;
@@ -753,10 +754,10 @@
val asm = if is_some b_statement then b_statement else a_statement;
val notes =
- if is_some asm
- then [(Thm.internalK, [((Binding.suffix_name ("_" ^ axiomsN) bname, []),
- [([Assumption.assume (cterm_of thy' (the asm))],
- [(Attrib.internal o K) Locale.witness_add])])])]
+ if is_some asm then
+ [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) bname), []),
+ [([Assumption.assume (cterm_of thy' (the asm))],
+ [(Attrib.internal o K) Locale.witness_add])])])]
else [];
val notes' = body_elems |>
--- a/src/Pure/Isar/locale.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/Pure/Isar/locale.ML Wed Oct 28 16:25:27 2009 +0100
@@ -553,7 +553,8 @@
fun add_decls add loc decl =
ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
add_thmss loc Thm.internalK
- [((Binding.empty, [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
+ [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
+ [([Drule.dummy_thm], [])])];
in
--- a/src/Pure/axclass.ML Wed Oct 28 16:25:26 2009 +0100
+++ b/src/Pure/axclass.ML Wed Oct 28 16:25:27 2009 +0100
@@ -311,7 +311,7 @@
(Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
#>> Thm.varifyT
#-> (fn thm => add_inst_param (c, tyco) (c'', thm)
- #> PureThy.add_thm ((Binding.name c', thm), [Thm.kind_internal])
+ #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [Thm.kind_internal])
#> snd
#> Sign.restore_naming thy
#> pair (Const (c, T))))