# HG changeset patch
# User wenzelm
# Date 1164128853 -3600
# Node ID a3c55b85cf0e6b5299d4f097f7cc74dc8b94c023
# Parent  5313a4cc382343b58294169e86954af7f90d786c
moved theorem kinds from PureThy to Thm;

diff -r 5313a4cc3823 -r a3c55b85cf0e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -432,7 +432,7 @@
 
 fun string_of_stmts state args =
   Proof.get_thmss state args
-  |> map (Element.pretty_statement (Proof.context_of state) PureThy.lemmaK)
+  |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
   |> Pretty.chunks2 |> Pretty.string_of;
 
 fun string_of_thms state args =
diff -r 5313a4cc3823 -r a3c55b85cf0e src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -239,10 +239,10 @@
   >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems kind args));
 
 val theoremsP =
-  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
+  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK);
 
 val lemmasP =
-  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK);
+  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK);
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
@@ -392,9 +392,9 @@
        Toplevel.local_theory_to_proof loc
          (Specification.theorem kind NONE (K I) a elems concl))));
 
-val theoremP = gen_theorem PureThy.theoremK;
-val lemmaP = gen_theorem PureThy.lemmaK;
-val corollaryP = gen_theorem PureThy.corollaryK;
+val theoremP = gen_theorem Thm.theoremK;
+val lemmaP = gen_theorem Thm.lemmaK;
+val corollaryP = gen_theorem Thm.corollaryK;
 
 val haveP =
   OuterSyntax.command "have" "state local goal"
diff -r 5313a4cc3823 -r a3c55b85cf0e src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/Isar/proof_display.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -121,7 +121,7 @@
   | print_results false = K (K ());
 
 fun present_results ctxt ((kind, name), res) =
-  if kind = "" orelse kind = PureThy.internalK then ()
+  if kind = "" orelse kind = Thm.internalK then ()
   else (print_results true ctxt ((kind, name), res);
     Context.setmp (SOME (ProofContext.theory_of ctxt))
       (Present.results kind) (name_results name res));
diff -r 5313a4cc3823 -r a3c55b85cf0e src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/drule.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -934,13 +934,13 @@
   val term_def = unvarify ProtoPure.term_def;
 in
   val protect = Thm.capply (cert Logic.protectC);
-  val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
+  val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
-  val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
+  val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
 
-  val termI = store_thm "termI" (PureThy.kind_rule PureThy.internalK (standard
+  val termI = store_thm "termI" (PureThy.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
 end;
 
diff -r 5313a4cc3823 -r a3c55b85cf0e src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Nov 21 18:07:32 2006 +0100
+++ b/src/Pure/thm.ML	Tue Nov 21 18:07:33 2006 +0100
@@ -70,6 +70,13 @@
     tpairs: (cterm * cterm) list,
     prop: cterm}
   exception THM of string * int * thm list
+  val axiomK: string
+  val assumptionK: string
+  val definitionK: string
+  val theoremK: string
+  val lemmaK: string
+  val corollaryK: string
+  val internalK: string
   type attribute     (* = Context.generic * thm -> Context.generic * thm *)
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
@@ -427,6 +434,14 @@
 fun merge_thys2 (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) =
   Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
 
+(*theorem kinds*)
+val axiomK = "axiom";
+val assumptionK = "assumption";
+val definitionK = "definition";
+val theoremK = "theorem";
+val lemmaK = "lemma";
+val corollaryK = "corollary";
+val internalK = "internal";
 
 (*attributes subsume any kind of rules or context modifiers*)
 type attribute = Context.generic * thm -> Context.generic * thm;