# HG changeset patch
# User wenzelm
# Date 1138384982 -3600
# Node ID f137c5e971f5425815c1b299e0c483ed38bed6d3
# Parent  ca02a20779550755e4feb49a80aa1cb764197c0c
moved theorem tags from Drule to PureThy;

diff -r ca02a2077955 -r f137c5e971f5 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -369,7 +369,7 @@
       [(("", proj index), [InductAttrib.induct_type name]),
        (("", exhaustion), [InductAttrib.cases_type name])];
     fun unnamed_rule i =
-      (("", proj i), [Drule.kind_internal, InductAttrib.induct_type ""]);
+      (("", proj i), [PureThy.kind_internal, InductAttrib.induct_type ""]);
   in
     PureThy.add_thms
       (List.concat (map named_rules infos) @
diff -r ca02a2077955 -r f137c5e971f5 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -570,7 +570,7 @@
 
     val facts = args |> map (fn ((a, atts), props) =>
      ((a, map (prep_att thy) atts), map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
+  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
 
 val inductive_cases = gen_inductive_cases Attrib.attribute ProofContext.read_prop;
 val inductive_cases_i = gen_inductive_cases (K I) ProofContext.cert_prop;
diff -r ca02a2077955 -r f137c5e971f5 src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -280,7 +280,7 @@
     val tc = List.nth (tcs, i - 1) handle Subscript =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
-  in IsarThy.theorem_i Drule.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
 
 val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);
diff -r ca02a2077955 -r f137c5e971f5 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -231,7 +231,7 @@
             fun post_proc (context, th) =
                 post_process (Context.theory_of context, th) |>> Context.Theory;
     in
-      IsarThy.theorem_i Drule.internalK
+      IsarThy.theorem_i PureThy.internalK
         ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
         (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
     end
diff -r ca02a2077955 -r f137c5e971f5 src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -256,7 +256,7 @@
     val (_, goal, goal_pat, att_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
     val att = #1 o att_result;
-  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
 
 in
 
diff -r ca02a2077955 -r f137c5e971f5 src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/HOLCF/pcpodef_package.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -178,7 +178,7 @@
   let
     val (goal, att) =
       gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
-  in IsarThy.theorem_i Drule.internalK ("", [att]) (goal, ([], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end;
 
 fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
 fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
diff -r ca02a2077955 -r f137c5e971f5 src/Provers/induct_method.ML
--- a/src/Provers/induct_method.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Provers/induct_method.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -363,7 +363,7 @@
 fun find_inductT ctxt insts =
   fold_rev multiply (insts |> List.mapPartial (fn [] => NONE | ts => List.last ts)
     |> map (InductAttrib.find_inductT ctxt o Term.fastype_of)) [[]]
-  |> filter_out (forall Drule.is_internal);
+  |> filter_out (forall PureThy.is_internal);
 
 fun find_inductS ctxt (fact :: _) = map single (InductAttrib.find_inductS ctxt (Thm.concl_of fact))
   | find_inductS _ _ = [];
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -202,8 +202,8 @@
 
 (* tags *)
 
-fun tagged x = syntax (tag >> Drule.tag) x;
-fun untagged x = syntax (Scan.lift Args.name >> Drule.untag) x;
+fun tagged x = syntax (tag >> PureThy.tag) x;
+fun untagged x = syntax (Scan.lift Args.name >> PureThy.untag) x;
 
 
 (* rule composition *)
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -212,10 +212,10 @@
   >> (Toplevel.theory_context o uncurry (IsarThy.smart_theorems kind));
 
 val theoremsP =
-  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Drule.theoremK);
+  OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems PureThy.theoremK);
 
 val lemmasP =
-  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Drule.lemmaK);
+  OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems PureThy.lemmaK);
 
 val declareP =
   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
@@ -322,7 +322,7 @@
     ((P.opt_keyword "open" >> not) -- P.name
         -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, [])
       >> (Toplevel.theory_context o (fn ((x, y), (z, w)) =>
-          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (thy, ctxt)))));
+          Locale.add_locale_context x y z w #> (fn ((_, ctxt), thy) => (ctxt, thy)))));
 
 val opt_inst =
   Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [];
@@ -359,9 +359,9 @@
       general_statement >> (fn ((x, y), (z, w)) =>
       (Toplevel.print o Toplevel.theory_to_proof (Locale.smart_theorem kind x y z w))));
 
-val theoremP = gen_theorem Drule.theoremK;
-val lemmaP = gen_theorem Drule.lemmaK;
-val corollaryP = gen_theorem Drule.corollaryK;
+val theoremP = gen_theorem PureThy.theoremK;
+val lemmaP = gen_theorem PureThy.lemmaK;
+val corollaryP = gen_theorem PureThy.corollaryK;
 
 val haveP =
   OuterSyntax.command "have" "state local goal"
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Isar/proof_display.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -65,7 +65,7 @@
   | print_results false = K (K ());
 
 fun present_results ctxt ((kind, name), res) =
-  if kind = "" orelse kind = Drule.internalK then ()
+  if kind = "" orelse kind = PureThy.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 ca02a2077955 -r f137c5e971f5 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -225,8 +225,8 @@
 
 fun put_consumes NONE th = th
   | put_consumes (SOME n) th = th
-      |> Drule.untag_rule consumes_tagN
-      |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]);
+      |> PureThy.untag_rule consumes_tagN
+      |> PureThy.tag_rule (consumes_tagN, [Library.string_of_int n]);
 
 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
 
@@ -244,8 +244,8 @@
 
 fun add_case_names NONE = I
   | add_case_names (SOME names) =
-      Drule.untag_rule case_names_tagN
-      #> Drule.tag_rule (case_names_tagN, names);
+      PureThy.untag_rule case_names_tagN
+      #> PureThy.tag_rule (case_names_tagN, names);
 
 fun lookup_case_names th = AList.lookup (op =) (Thm.tags_of_thm th) case_names_tagN;
 
@@ -262,7 +262,7 @@
 fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name)
   | is_case_concl _ _ = false;
 
-fun add_case_concl (name, cs) = Drule.map_tags (fn tags =>
+fun add_case_concl (name, cs) = PureThy.map_tags (fn tags =>
   filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
 
 fun get_case_concls th name =
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -39,7 +39,7 @@
   | make_deps_graph prf = (fn p as (gra, parents) =>
       let val ((name, tags), prf') = dest_thm_axm prf
       in
-        if name <> "" andalso not (Drule.has_internal tags) then
+        if name <> "" andalso not (PureThy.has_internal tags) then
           if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph prf' (gra, []);
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/axclass.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -306,7 +306,7 @@
 fun gen_instance mk_prop add_thms after_qed inst thy =
   thy
   |> ProofContext.init
-  |> Proof.theorem_i Drule.internalK NONE (after_qed oo fold add_thms) NONE ("", [])
+  |> Proof.theorem_i PureThy.internalK NONE (after_qed oo fold add_thms) NONE ("", [])
        (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
 
 in
diff -r ca02a2077955 -r f137c5e971f5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/Pure/drule.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -92,20 +92,6 @@
   val beta_conv: cterm -> cterm -> cterm
   val plain_prop_of: thm -> term
   val add_used: thm -> string list -> string list
-  val map_tags: (tag list -> tag list) -> thm -> thm
-  val tag_rule: tag -> thm -> thm
-  val untag_rule: string -> thm -> thm
-  val tag: tag -> attribute
-  val untag: string -> attribute
-  val get_kind: thm -> string
-  val kind: string -> attribute
-  val theoremK: string
-  val lemmaK: string
-  val corollaryK: string
-  val internalK: string
-  val kind_internal: attribute
-  val has_internal: tag list -> bool
-  val is_internal: thm -> bool
   val flexflex_unique: thm -> thm
   val close_derivation: thm -> thm
   val local_standard: thm -> thm
@@ -322,42 +308,6 @@
 
 
 
-(** theorem tags **)
-
-(* add / delete tags *)
-
-fun map_tags f thm =
-  Thm.put_name_tags (Thm.name_of_thm thm, f (#2 (Thm.get_name_tags thm))) thm;
-
-fun tag_rule tg = map_tags (fn tgs => if tg mem tgs then tgs else tgs @ [tg]);
-fun untag_rule s = map_tags (filter_out (equal s o #1));
-
-fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
-fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
-
-fun simple_tag name x = tag (name, []) x;
-
-
-(* theorem kinds *)
-
-val theoremK = "theorem";
-val lemmaK = "lemma";
-val corollaryK = "corollary";
-val internalK = "internal";
-
-fun get_kind thm =
-  (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
-    SOME (k :: _) => k
-  | _ => "unknown");
-
-fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
-fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
-fun kind_internal x = kind internalK x;
-fun has_internal tags = exists (fn ("kind", [k]) => k = internalK | _ => false) tags;
-val is_internal = has_internal o Thm.tags_of_thm;
-
-
-
 (** Standardization of rules **)
 
 (*vars in left-to-right order*)
@@ -984,9 +934,9 @@
   val prop_def = #1 (freeze_thaw ProtoPure.prop_def);
 in
   val protect = Thm.capply (cert Logic.protectC);
-  val protectI = store_thm "protectI" (kind_rule internalK (standard
+  val protectI = store_thm "protectI" (PureThy.kind_rule PureThy.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
-  val protectD = store_thm "protectD" (kind_rule internalK (standard
+  val protectD = store_thm "protectD" (PureThy.kind_rule PureThy.internalK (standard
       (Thm.equal_elim prop_def (Thm.assume (protect A)))));
   val protect_cong = store_standard_thm_open "protect_cong" (Thm.reflexive (protect A));
 end;
diff -r ca02a2077955 -r f137c5e971f5 src/ZF/Tools/ind_cases.ML
--- a/src/ZF/Tools/ind_cases.ML	Fri Jan 27 18:29:33 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML	Fri Jan 27 19:03:02 2006 +0100
@@ -55,7 +55,7 @@
     val facts = args |> map (fn ((name, srcs), props) =>
       ((name, map (Attrib.attribute thy) srcs),
         map (Thm.no_attributes o single o mk_cases) props));
-  in thy |> IsarThy.theorems_i Drule.lemmaK facts |> snd end;
+  in thy |> IsarThy.theorems_i PureThy.lemmaK facts |> snd end;
 
 
 (* ind_cases method *)