--- a/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 14:32:21 2009 -0800
@@ -569,7 +569,7 @@
thy3
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ {quiet_mode = false, verbose = false, kind = "",
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))
@@ -1513,7 +1513,7 @@
thy10
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
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))
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Nov 12 14:32:21 2009 -0800
@@ -156,7 +156,7 @@
thy0
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
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))
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Nov 12 14:32:21 2009 -0800
@@ -175,7 +175,7 @@
thy1
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
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') []
--- a/src/HOL/Tools/Function/function_core.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/Function/function_core.ML Thu Nov 12 14:32:21 2009 -0800
@@ -460,7 +460,7 @@
|> Inductive.add_inductive_i
{quiet_mode = true,
verbose = ! trace,
- kind = Thm.internalK,
+ kind = "",
alt_name = Binding.empty,
coind = false,
no_elim = false,
@@ -519,7 +519,7 @@
$ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
|> Syntax.check_term lthy
in
- LocalTheory.define Thm.internalK
+ LocalTheory.define ""
((Binding.name (function_name fname), mixfix),
((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
end
--- a/src/HOL/Tools/Function/mutual.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/Function/mutual.ML Thu Nov 12 14:32:21 2009 -0800
@@ -146,7 +146,7 @@
fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
let
val ((f, (_, f_defthm)), lthy') =
- LocalTheory.define Thm.internalK
+ LocalTheory.define ""
((Binding.name fname, mixfix),
((Binding.conceal (Binding.name (fname ^ "_def")), []),
Term.subst_bound (fsum, f_def))) lthy
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 14:32:21 2009 -0800
@@ -355,7 +355,7 @@
thy
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ {quiet_mode = false, verbose = false, kind = "",
alt_name = Binding.empty, coind = false, no_elim = false,
no_ind = false, skip_mono = false, fork_mono = false}
(map (fn (s, T) =>
--- a/src/HOL/Tools/inductive.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/inductive.ML Thu Nov 12 14:32:21 2009 -0800
@@ -663,7 +663,7 @@
val ((rec_const, (_, fp_def)), lthy') = lthy
|> LocalTheory.conceal
- |> LocalTheory.define Thm.internalK
+ |> LocalTheory.define ""
((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
fold_rev lambda params
@@ -686,13 +686,13 @@
end) (cnames_syn ~~ cs);
val (consts_defs, lthy'') = lthy'
|> LocalTheory.conceal
- |> fold_map (LocalTheory.define Thm.internalK) specs
+ |> fold_map (LocalTheory.define "") specs
||> LocalTheory.restore_naming lthy';
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 lthy'';
val ((_, [mono']), lthy''') =
- LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+ LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
list_comb (rec_const, params), preds, argTs, bs, xs)
--- a/src/HOL/Tools/inductive_set.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/inductive_set.ML Thu Nov 12 14:32:21 2009 -0800
@@ -485,7 +485,7 @@
(* define inductive sets using previously defined predicates *)
val (defs, lthy2) = lthy1
|> LocalTheory.conceal (* FIXME ?? *)
- |> fold_map (LocalTheory.define Thm.internalK)
+ |> fold_map (LocalTheory.define "")
(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))))))
--- a/src/HOL/Tools/recdef.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/HOL/Tools/recdef.ML Thu Nov 12 14:32:21 2009 -0800
@@ -263,7 +263,7 @@
error ("No termination condition #" ^ string_of_int i ^
" in recdef definition of " ^ quote name);
in
- Specification.theorem Thm.internalK NONE (K I)
+ Specification.theorem "" NONE (K I)
(Binding.conceal (Binding.name bname), atts) []
(Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
end;
--- a/src/Pure/General/markup.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/General/markup.ML Thu Nov 12 14:32:21 2009 -0800
@@ -14,7 +14,6 @@
val name: string -> T -> T
val bindingN: string val binding: string -> T
val kindN: string
- val internalK: string
val entityN: string val entity: string -> T
val defN: string
val refN: string
@@ -154,8 +153,6 @@
val kindN = "kind";
-val internalK = "internal";
-
(* formal entities *)
--- a/src/Pure/Isar/expression.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Isar/expression.ML Thu Nov 12 14:32:21 2009 -0800
@@ -682,7 +682,7 @@
val (_, thy'') =
thy'
|> Sign.mandatory_path (Binding.name_of abinding)
- |> PureThy.note_thmss Thm.internalK
+ |> PureThy.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
||> Sign.restore_naming thy';
in (SOME statement, SOME intro, axioms, thy'') end;
@@ -696,7 +696,7 @@
val (_, thy'''') =
thy'''
|> Sign.mandatory_path (Binding.name_of binding)
- |> PureThy.note_thmss Thm.internalK
+ |> PureThy.note_thmss ""
[((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
((Binding.conceal (Binding.name axiomsN), []),
[(map (Drule.standard o Element.conclude_witness) axioms, [])])]
@@ -713,7 +713,7 @@
fold_map (fn (a, spec) => fn axs =>
let val (ps, qs) = chop (length spec) axs
in ((a, [(ps, [])]), qs) end) asms axms
- |> apfst (curry Notes Thm.assumptionK)
+ |> apfst (curry Notes "")
| assumes_to_notes e axms = (e, axms);
fun defines_to_notes thy (Defines defs) =
@@ -755,7 +755,7 @@
val notes =
if is_some asm then
- [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
+ [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
[([Assumption.assume (cterm_of thy' (the asm))],
[(Attrib.internal o K) Locale.witness_add])])])]
else [];
--- a/src/Pure/Isar/locale.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Isar/locale.ML Thu Nov 12 14:32:21 2009 -0800
@@ -518,7 +518,7 @@
fun add_decls add loc decl =
ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
- add_thmss loc Thm.internalK
+ add_thmss loc ""
[((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
[([Drule.dummy_thm], [])])];
--- a/src/Pure/Isar/proof_context.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Isar/proof_context.ML Thu Nov 12 14:32:21 2009 -0800
@@ -1126,7 +1126,7 @@
in
ctxt2
|> auto_bind_facts (flat propss)
- |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+ |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
end;
in
--- a/src/Pure/Isar/proof_display.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Isar/proof_display.ML Thu Nov 12 14:32:21 2009 -0800
@@ -91,7 +91,7 @@
in
fun print_results do_print ctxt ((kind, name), facts) =
- if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
+ if not do_print orelse kind = "" then ()
else if name = "" then
Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
else Pretty.writeln
--- a/src/Pure/Isar/specification.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Isar/specification.ML Thu Nov 12 14:32:21 2009 -0800
@@ -172,7 +172,7 @@
#>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
(*facts*)
- val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
+ val (facts, thy') = axioms_thy |> PureThy.note_thmss ""
(Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
val _ =
@@ -329,8 +329,9 @@
val (facts, goal_ctxt) = elems_ctxt
|> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
|> fold_map assume_case (obtains ~~ propp)
- |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
- [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+ |-> (fn ths =>
+ ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+ #2 #> pair ths);
in ((prems, stmt, SOME facts), goal_ctxt) end);
structure TheoremHook = Generic_Data
@@ -372,8 +373,7 @@
end;
in
goal_ctxt
- |> ProofContext.note_thmss Thm.assumptionK
- [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
+ |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
|> snd
|> Proof.theorem_i before_qed after_qed' (map snd stmt)
|> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
--- a/src/Pure/Thy/thm_deps.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/Thy/thm_deps.ML Thu Nov 12 14:32:21 2009 -0800
@@ -79,9 +79,7 @@
NONE => I
| SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
- if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
- (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
- then
+ if not concealed andalso is_unused (a, th) then
(case group of
NONE => ((a, th) :: thms, grps')
| SOME grp =>
--- a/src/Pure/drule.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/drule.ML Thu Nov 12 14:32:21 2009 -0800
@@ -710,13 +710,11 @@
val protectI =
store_thm (Binding.conceal (Binding.name "protectI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
+ (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
val protectD =
store_thm (Binding.conceal (Binding.name "protectD"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+ (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
val protect_cong =
store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
@@ -734,8 +732,7 @@
val termI =
store_thm (Binding.conceal (Binding.name "termI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
+ (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
fun mk_term ct =
let
@@ -764,15 +761,14 @@
val sort_constraintI =
store_thm (Binding.conceal (Binding.name "sort_constraintI"))
- (Thm.kind_rule Thm.internalK (standard
- (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
+ (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
val sort_constraint_eq =
store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
- (Thm.kind_rule Thm.internalK (standard
+ (standard
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
- (implies_intr_list [A, C] (Thm.assume A)))));
+ (implies_intr_list [A, C] (Thm.assume A))));
end;
--- a/src/Pure/more_thm.ML Thu Nov 12 14:31:29 2009 -0800
+++ b/src/Pure/more_thm.ML Thu Nov 12 14:32:21 2009 -0800
@@ -84,14 +84,11 @@
val has_name_hint: thm -> bool
val get_name_hint: thm -> string
val put_name_hint: string -> thm -> thm
- val axiomK: string
- val assumptionK: string
val definitionK: string
val theoremK: string
val generatedK : string
val lemmaK: string
val corollaryK: string
- val internalK: string
val get_kind: thm -> string
val kind_rule: string -> thm -> thm
val kind: string -> attribute
@@ -414,14 +411,11 @@
(* theorem kinds *)
-val axiomK = "axiom";
-val assumptionK = "assumption";
val definitionK = "definition";
val theoremK = "theorem";
val generatedK = "generatedK"
val lemmaK = "lemma";
val corollaryK = "corollary";
-val internalK = Markup.internalK;
fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);