# HG changeset patch # User wenzelm # Date 1444131104 -7200 # Node ID fa4ebbd350ae0a10177b2eff2d117e5e0b1d62bc # Parent 43848476063ca53ea78ba3e82a080419fde11042 just one theorem kind, which is legacy anyway; diff -r 43848476063c -r fa4ebbd350ae src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML Tue Oct 06 13:31:44 2015 +0200 @@ -111,7 +111,7 @@ #-> Class.prove_instantiation_exit_result (map o Morphism.thm) tac o single #-> fold Code.del_eqn #> `(mk_free_ctr_equations fcT ctrs inject_thms distinct_thms) - #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.lemmaK + #-> (fn (thms, thm) => Global_Theory.note_thmss Thm.theoremK [((qualify reflN, [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), ((qualify simpsN, [Code.add_default_eqn_attribute]), [(rev thms, [])])]) #> snd diff -r 43848476063c -r fa4ebbd350ae src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/Pure/Isar/expression.ML Tue Oct 06 13:31:44 2015 +0200 @@ -888,7 +888,7 @@ val facts = map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; val (eqns', ctxt') = ctxt - |> note Thm.lemmaK facts + |> note Thm.theoremK facts |> (fn (eqns, ctxt') => (meta_rewrite ctxt' eqns, ctxt')); val dep_morphs = map2 (fn (dep, morph) => fn wits => diff -r 43848476063c -r fa4ebbd350ae src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/Pure/Isar/isar_syn.ML Tue Oct 06 13:31:44 2015 +0200 @@ -152,16 +152,15 @@ (* theorems *) -fun theorems kind = +val theorems = Parse_Spec.name_facts -- Parse.for_fixes - >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes); + >> (fn (facts, fixes) => #2 oo Specification.theorems_cmd Thm.theoremK facts fixes); val _ = - Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems" - (theorems Thm.theoremK); + Outer_Syntax.local_theory' @{command_keyword theorems} "define theorems" theorems; val _ = - Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" (theorems Thm.lemmaK); + Outer_Syntax.local_theory' @{command_keyword lemmas} "define lemmas" theorems; val _ = Outer_Syntax.local_theory' @{command_keyword declare} "declare theorems" @@ -494,23 +493,23 @@ (* statements *) -fun theorem spec schematic kind = +fun theorem spec schematic descr = Outer_Syntax.local_theory_to_proof' spec - ("state " ^ (if schematic then "schematic " ^ kind else kind)) + ("state " ^ descr) (Scan.optional (Parse_Spec.opt_thm_name ":" --| Scan.ahead (Parse_Spec.includes >> K "" || Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding -- Scan.optional Parse_Spec.includes [] -- Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) => ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd) - kind NONE (K I) a includes elems concl))); + Thm.theoremK NONE (K I) a includes elems concl))); -val _ = theorem @{command_keyword theorem} false Thm.theoremK; -val _ = theorem @{command_keyword lemma} false Thm.lemmaK; -val _ = theorem @{command_keyword corollary} false Thm.corollaryK; -val _ = theorem @{command_keyword schematic_theorem} true Thm.theoremK; -val _ = theorem @{command_keyword schematic_lemma} true Thm.lemmaK; -val _ = theorem @{command_keyword schematic_corollary} true Thm.corollaryK; +val _ = theorem @{command_keyword theorem} false "theorem"; +val _ = theorem @{command_keyword lemma} false "lemma"; +val _ = theorem @{command_keyword corollary} false "corollary"; +val _ = theorem @{command_keyword schematic_theorem} true "schematic goal"; +val _ = theorem @{command_keyword schematic_lemma} true "schematic goal"; +val _ = theorem @{command_keyword schematic_corollary} true "schematic goal"; val structured_statement = diff -r 43848476063c -r fa4ebbd350ae src/Pure/Tools/thm_deps.ML --- a/src/Pure/Tools/thm_deps.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/Pure/Tools/thm_deps.ML Tue Oct 06 13:31:44 2015 +0200 @@ -92,8 +92,7 @@ val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, seen_groups) => if not concealed andalso (* FIXME replace by robust treatment of thm groups *) - member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK] (Thm.legacy_get_kind th) andalso - is_unused a + Thm.legacy_get_kind th = Thm.theoremK andalso is_unused a then (case group of NONE => ((a, th) :: thms, seen_groups) diff -r 43848476063c -r fa4ebbd350ae src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/Pure/more_thm.ML Tue Oct 06 13:31:44 2015 +0200 @@ -101,8 +101,6 @@ val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm val theoremK: string - val lemmaK: string - val corollaryK: string val legacy_get_kind: thm -> string val kind_rule: string -> thm -> thm val kind: string -> attribute @@ -576,8 +574,6 @@ (* theorem kinds *) val theoremK = "theorem"; -val lemmaK = "lemma"; -val corollaryK = "corollary"; fun legacy_get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN); diff -r 43848476063c -r fa4ebbd350ae src/Tools/permanent_interpretation.ML --- a/src/Tools/permanent_interpretation.ML Tue Oct 06 11:29:00 2015 +0200 +++ b/src/Tools/permanent_interpretation.ML Tue Oct 06 13:31:44 2015 +0200 @@ -59,7 +59,7 @@ val facts = (Attrib.empty_binding, [(map (Morphism.thm (export' $> export)) def_eqns, [])]) :: map2 (fn attrs => fn eqn => (attrs, [([Morphism.thm (export' $> export) eqn], [])])) attrss eqns; val (eqns', ctxt') = ctxt - |> note Thm.lemmaK facts + |> note Thm.theoremK facts |-> meta_rewrite; val dep_morphs = map2 (fn (dep, morph) => fn wits => (dep, morph $> Element.satisfy_morphism (map (Element.transform_witness export') wits))) deps witss; @@ -71,9 +71,9 @@ end; fun generic_interpretation prep_interpretation setup_proof note add_registration - expression raw_defs raw_eqns initial_ctxt = + expression raw_defs raw_eqns initial_ctxt = let - val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = + val (((propss, deps, export, export'), (def_eqns, eqns, attrss)), goal_ctxt) = prep_interpretation expression raw_defs raw_eqns initial_ctxt; fun after_qed witss eqns = note_eqns_register note add_registration deps witss def_eqns eqns attrss export export';