# HG changeset patch # User wenzelm # Date 1258059731 -3600 # Node ID b275f26a638b0cecec75e1e439527778179a1ff0 # Parent d983509dbf31004fa8e5a6681501e8532a19d2f6 eliminated obsolete "internal" kind -- collapsed to unspecific ""; diff -r d983509dbf31 -r b275f26a638b src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/Datatype/datatype_abs_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/Datatype/datatype_rep_proofs.ML --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/Function/function_core.ML --- a/src/HOL/Tools/Function/function_core.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/Function/function_core.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/Function/mutual.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/inductive.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/inductive_set.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/HOL/Tools/recdef.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/General/markup.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/Isar/expression.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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, [])])] @@ -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 d983509dbf31 -r b275f26a638b src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/Isar/locale.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/Isar/proof_display.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/drule.ML Thu Nov 12 22:02:11 2009 +0100 @@ -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 d983509dbf31 -r b275f26a638b src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Nov 12 21:59:35 2009 +0100 +++ b/src/Pure/more_thm.ML Thu Nov 12 22:02:11 2009 +0100 @@ -91,7 +91,6 @@ 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 @@ -421,7 +420,6 @@ 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);