--- 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
--- 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 =>
--- 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 =
--- 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)
--- 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);
--- 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';