moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);

--- a/src/HOL/Import/shuffler.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -627,7 +627,7 @@
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
         val all_thms =
-          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
+          map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     in
         List.filter (match_consts ignored t) all_thms
     end

--- a/src/HOL/Tools/datatype_package.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -217,7 +217,7 @@
       [(("", nth inducts index), [Induct.induct_type name]),
        (("", exhaustion), [Induct.cases_type name])];
     fun unnamed_rule i =
-      (("", nth inducts i), [PureThy.kind_internal, Induct.induct_type ""]);
+      (("", nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
   in
     thy |> PureThy.add_thms
       (maps named_rules infos @

--- a/src/HOL/Tools/meson.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -431,7 +431,7 @@
 (*Use "theorem naming" to label the clauses*)
 fun name_thms label =
     let fun name1 (th, (k,ths)) =
-          (k-1, PureThy.put_name_hint (label ^ string_of_int k) th :: ths)
+          (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
     in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
 
 (*Is the given disjunction an all-negative support clause?*)

--- a/src/HOL/Tools/metis_tools.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -568,7 +568,7 @@
   (* Main function to start metis prove and reconstruction *)
   fun FOL_SOLVE mode ctxt cls ths0 =
     let val thy = ProofContext.theory_of ctxt
-        val th_cls_pairs = map (fn th => (PureThy.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
+        val th_cls_pairs = map (fn th => (Thm.get_name_hint th, ResAxioms.cnf_axiom thy th)) ths0
         val ths = List.concat (map #2 th_cls_pairs)
         val _ = if exists(is_false o prop_of) cls then error "problem contains the empty clause"
                 else ();

--- a/src/HOL/Tools/res_atp.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -817,7 +817,7 @@
 fun sledgehammer state =
   let
     val (ctxt, (chain_ths, goal)) = Proof.get_goal (Toplevel.proof_of state)
-    val chain_ths = map (PureThy.put_name_hint Recon.chained_hint) chain_ths
+    val chain_ths = map (Thm.put_name_hint Recon.chained_hint) chain_ths
                     (*Mark the chained theorems to keep them out of metis calls;
                       their original "name hints" may be bad anyway.*)
     val thy = ProofContext.theory_of ctxt

--- a/src/HOL/Tools/res_axioms.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -327,7 +327,7 @@
     | _ => false;
 
 fun bad_for_atp th =
-  PureThy.is_internal th
+  Thm.is_internal th
   orelse too_complex (prop_of th)
   orelse exists_type type_has_empty_sort (prop_of th)
   orelse is_strange_thm th;
@@ -340,11 +340,11 @@
 fun flatten_name s = space_implode "_X" (NameSpace.explode s);
 
 fun fake_name th =
-  if PureThy.has_name_hint th then flatten_name (PureThy.get_name_hint th)
+  if Thm.has_name_hint th then flatten_name (Thm.get_name_hint th)
   else gensym "unknown_thm_";
 
 fun name_or_string th =
-  if PureThy.has_name_hint th then PureThy.get_name_hint th
+  if Thm.has_name_hint th then Thm.get_name_hint th
   else Display.string_of_thm th;
 
 (*Skolemize a named theorem, with Skolem functions as additional premises.*)
@@ -404,7 +404,7 @@
 
 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
 
-fun pairname th = (PureThy.get_name_hint th, th);
+fun pairname th = (Thm.get_name_hint th, th);
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs

--- a/src/HOL/Tools/res_reconstruct.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -488,7 +488,7 @@
 
 (**** retrieve the axioms that were used in the proof ****)
 
-(*PureThy.get_name_hint returns "??.unknown" if no name is available.*)
+(*Thm.get_name_hint returns "??.unknown" if no name is available.*)
 fun goodhint x = (x <> "??.unknown");  
 
 (*Get names of axioms used. Axioms are indexed from 1, while the vector is indexed from 0*)

--- a/src/HOL/ex/Quickcheck.thy	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Thu Aug 14 16:52:46 2008 +0200
@@ -121,7 +121,7 @@
                 |> singleton (ProofContext.export lthy (ProofContext.init thy))
             in
               lthy
-              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [PureThy.kind_internal])
+              |> LocalTheory.theory (PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
                    #-> Code.add_func)
             end;
         in

--- a/src/Pure/Isar/attrib.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -215,10 +215,10 @@
 
 (* tags *)
 
-val tagged = syntax (Scan.lift (Args.name -- Args.name) >> PureThy.tag);
-val untagged = syntax (Scan.lift Args.name >> PureThy.untag);
+val tagged = syntax (Scan.lift (Args.name -- Args.name) >> Thm.tag);
+val untagged = syntax (Scan.lift Args.name >> Thm.untag);
 
-val kind = syntax (Scan.lift Args.name >> PureThy.kind);
+val kind = syntax (Scan.lift Args.name >> Thm.kind);
 
 
 (* rule composition *)

--- a/src/Pure/Isar/element.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/element.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -228,9 +228,9 @@
 
 fun thm_name kind th prts =
   let val head =
-    if PureThy.has_name_hint th then
+    if Thm.has_name_hint th then
       Pretty.block [Pretty.command kind,
-        Pretty.brk 1, Pretty.str (Sign.base_name (PureThy.get_name_hint th) ^ ":")]
+        Pretty.brk 1, Pretty.str (Sign.base_name (Thm.get_name_hint th) ^ ":")]
     else Pretty.command kind
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
 

--- a/src/Pure/Isar/locale.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -1775,7 +1775,7 @@
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
       |> Sign.declare_const [] (bname, predT, NoSyn) |> snd
       |> PureThy.add_defs false
-        [((Thm.def_name bname, Logic.mk_equals (head, body)), [PureThy.kind_internal])];
+        [((Thm.def_name bname, Logic.mk_equals (head, body)), [Thm.kind_internal])];
     val defs_ctxt = ProofContext.init defs_thy |> Variable.declare_term head;
 
     val cert = Thm.cterm_of defs_thy;

--- a/src/Pure/Isar/rule_cases.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Isar/rule_cases.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -223,8 +223,8 @@
 
 fun put_consumes NONE th = th
   | put_consumes (SOME n) th = th
-      |> PureThy.untag_rule consumes_tagN
-      |> PureThy.tag_rule
+      |> Thm.untag_rule consumes_tagN
+      |> Thm.tag_rule
         (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n));
 
 fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th;
@@ -247,8 +247,8 @@
 
 fun add_case_names NONE = I
   | add_case_names (SOME names) =
-      PureThy.untag_rule case_names_tagN
-      #> PureThy.tag_rule (case_names_tagN, implode_args names);
+      Thm.untag_rule case_names_tagN
+      #> Thm.tag_rule (case_names_tagN, implode_args names);
 
 fun lookup_case_names th =
   AList.lookup (op =) (Thm.get_tags th) case_names_tagN

--- a/src/Pure/Proof/extraction.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Proof/extraction.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -356,7 +356,7 @@
     val is_def =
       (case strip_comb (fst (Logic.dest_equals (prop_of thm))) of
          (Const _, ts) => forall is_Var ts andalso not (has_duplicates (op =) ts)
-           andalso (PureThy.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
+           andalso (Thm.get_kind thm = Thm.definitionK orelse can (Thm.get_axiom_i thy) name)
        | _ => false) handle TERM _ => false;
   in
     (ExtractionData.put (if is_def then

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -176,7 +176,7 @@
 fun tell_thm_deps ths =
   if print_mode_active thm_depsN then
     let
-      val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
+      val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
       val deps = Symtab.keys (fold Proofterm.thms_of_proof'
 				   (map Thm.proof_of ths) Symtab.empty);
     in

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -341,7 +341,7 @@
 fun tell_thm_deps ths =
   if !show_theorem_dependencies then
       let
-        val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths);
+        val names = map Thm.get_name_hint (filter Thm.has_name_hint ths);
         val deps = (Symtab.keys (fold Proofterm.thms_of_proof'
                                         (map Thm.proof_of ths) Symtab.empty))
       in

--- a/src/Pure/Thy/thm_deps.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -93,13 +93,13 @@
       | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
     (* groups containing at least one used theorem *)
     val grps = fold (fn p as (_, thm) => if is_unused p then I else
-      case PureThy.get_group thm of
+      case Thm.get_group thm of
         NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
     val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
-      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
+      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
         andalso is_unused p
       then
-        (case PureThy.get_group thm of
+        (case Thm.get_group thm of
            NONE => (p :: thms, grps')
          | SOME grp =>
              (* do not output theorem if another theorem in group has been used *)

--- a/src/Pure/axclass.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/axclass.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -374,7 +374,7 @@
           (Thm.def_name c', Logic.mk_equals (Const (c, T'), const'))
     #>> Thm.varifyT
     #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
-    #> PureThy.add_thm ((c', thm), [PureThy.kind_internal])
+    #> PureThy.add_thm ((c', thm), [Thm.kind_internal])
     #> snd
     #> Sign.restore_naming thy
     #> pair (Const (c, T))))

--- a/src/Pure/drule.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/drule.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -791,13 +791,13 @@
   val term_def = get_axiom "term_def";
 in
   val protect = Thm.capply (certify Logic.protectC);
-  val protectI = store_thm "protectI" (PureThy.kind_rule Thm.internalK (standard
+  val protectI = store_thm "protectI" (Thm.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
-  val protectD = store_thm "protectD" (PureThy.kind_rule Thm.internalK (standard
+  val protectD = store_thm "protectD" (Thm.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 Thm.internalK (standard
+  val termI = store_thm "termI" (Thm.kind_rule Thm.internalK (standard
       (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
 end;
 

--- a/src/Pure/meta_simplifier.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -528,7 +528,7 @@
   end;
 
 fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
+  maps (fn thm => map (rpair (Thm.get_name_hint thm)) (mk thm)) thms;
 
 fun extract_safe_rrules (ss, thm) =
   maps (orient_rrule ss) (extract_rews (ss, [thm]));

--- a/src/Pure/pure_thy.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Pure/pure_thy.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -7,23 +7,6 @@
 
 signature PURE_THY =
 sig
-  val tag_rule: Markup.property -> thm -> thm
-  val untag_rule: string -> thm -> thm
-  val tag: Markup.property -> attribute
-  val untag: string -> attribute
-  val has_name_hint: thm -> bool
-  val get_name_hint: thm -> string
-  val put_name_hint: string -> thm -> thm
-  val get_group: thm -> string option
-  val put_group: string -> thm -> thm
-  val group: string -> attribute
-  val has_kind: thm -> bool
-  val get_kind: thm -> string
-  val kind_rule: string -> thm -> thm
-  val kind: string -> attribute
-  val kind_internal: attribute
-  val has_internal: Markup.property list -> bool
-  val is_internal: thm -> bool
   val facts_of: theory -> Facts.T
   val intern_fact: theory -> xstring -> string
   val defined_fact: theory -> string -> bool
@@ -69,52 +52,6 @@
 struct
 
 
-(*** theorem tags ***)
-
-(* add / delete tags *)
-
-fun tag_rule tg = Thm.map_tags (insert (op =) tg);
-fun untag_rule s = Thm.map_tags (filter_out (fn (s', _) => s = s'));
-
-fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x;
-fun untag s x = Thm.rule_attribute (K (untag_rule s)) x;
-
-
-(* unofficial theorem names *)
-
-fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN);
-
-val has_name_hint = can the_name_hint;
-val get_name_hint = the_default "??.unknown" o try the_name_hint;
-
-fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name);
-
-
-(* theorem groups *)
-
-fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN;
-
-fun put_group name =
-  if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name));
-
-fun group name = Thm.rule_attribute (K (put_group name));
-
-
-(* theorem kinds *)
-
-fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN);
-
-val has_kind = can the_kind;
-val get_kind = the_default "" o try the_kind;
-
-fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN;
-fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x;
-fun kind_internal x = kind Thm.internalK x;
-fun has_internal tags = exists (fn tg => tg = (Markup.kindN, Thm.internalK)) tags;
-val is_internal = has_internal o Thm.get_tags;
-
-
-
 (*** stored facts ***)
 
 (** theory data **)
@@ -159,7 +96,7 @@
 fun get_thm thy name = Facts.the_single name (get_thms thy name);
 
 fun all_thms_of thy =
-  Facts.fold_static (fn (_, ths) => append (map (`(get_name_hint)) ths)) (facts_of thy) [];
+  Facts.fold_static (fn (_, ths) => append (map (`(Thm.get_name_hint)) ths)) (facts_of thy) [];
 
 
 
@@ -180,8 +117,8 @@
 
 fun name_thm pre official name thm = thm
   |> (if Thm.get_name thm <> "" andalso pre orelse not official then I else Thm.put_name name)
-  |> (if has_name_hint thm andalso pre orelse name = "" then I else put_name_hint name)
-  |> Thm.map_tags (Position.default_properties (Position.thread_data ()));
+  |> (if Thm.has_name_hint thm andalso pre orelse name = "" then I else Thm.put_name_hint name)
+  |> Thm.default_position (Position.thread_data ());
 
 fun name_thms pre official name xs =
   map (uncurry (name_thm pre official)) (name_multi name xs);
@@ -250,8 +187,8 @@
 
 in
 
-fun note_thmss k = gen_note_thmss (kind k);
-fun note_thmss_grouped k g = gen_note_thmss (kind k #> group g);
+fun note_thmss k = gen_note_thmss (Thm.kind k);
+fun note_thmss_grouped k g = gen_note_thmss (Thm.kind k #> Thm.group g);
 
 end;
 
@@ -414,4 +351,3 @@
   #> Theory.add_axioms_i Proofterm.equality_axms));
 
 end;
-

--- a/src/Tools/induct.ML	Thu Aug 14 11:55:05 2008 +0200
+++ b/src/Tools/induct.ML	Thu Aug 14 16:52:46 2008 +0200
@@ -573,7 +573,7 @@
       ((fn [] => NONE | ts => List.last ts) #>
         (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
         find_inductT ctxt)) [[]]
-  |> filter_out (forall PureThy.is_internal);
+  |> filter_out (forall Thm.is_internal);
 
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];