# HG changeset patch # User huffman # Date 1258065141 28800 # Node ID 555e5358b8c9bc5939628895ba6333a6810c296d # Parent 053ac8080c11aebc72e35cfad691e42bf6ce9a21# Parent 5266a72e08895e186e00161f171db3e1425a888a merged diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Nominal/nominal_datatype.ML --- 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)) diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- 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)) diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- 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') [] diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/Function/function_core.ML --- 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 diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/Function/mutual.ML --- 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 diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- 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) => diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/inductive.ML --- 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) diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/inductive_set.ML --- 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)))))) diff -r 053ac8080c11 -r 555e5358b8c9 src/HOL/Tools/recdef.ML --- 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; diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/General/markup.ML --- 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 *) diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Isar/expression.ML --- 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 []; diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Isar/locale.ML --- 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], [])])]; diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Isar/proof_context.ML --- 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 diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Isar/proof_display.ML --- 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 diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Isar/specification.ML --- 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) diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/Thy/thm_deps.ML --- 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 => diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/drule.ML --- 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; diff -r 053ac8080c11 -r 555e5358b8c9 src/Pure/more_thm.ML --- 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);