thm/prf: separate official name vs. additional tags;

--- a/src/HOL/Import/xmlconv.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Import/xmlconv.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -143,7 +143,7 @@
   | xml_of_proof (prf %% prf') =
       XML.Elem ("AppP", [], [xml_of_proof prf, xml_of_proof prf'])
   | xml_of_proof (Hyp t) = XML.Elem ("Hyp", [], [xml_of_term t])
-  | xml_of_proof (PThm ((s, _), _, t, optTs)) =
+  | xml_of_proof (PThm (s, _, t, optTs)) =
       XML.Elem ("PThm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)
   | xml_of_proof (PAxm (s, t, optTs)) =
       XML.Elem ("PAxm", [("name", s)], xml_of_term t :: xml_of_opttypes optTs)

--- a/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -301,7 +301,7 @@
 (*Name management for ATP linkup. The suffix here must agree with the one given
   for notE in Clasimp.addIff*)
 fun name_notE th =
-    Thm.name_thm (Thm.name_of_thm th ^ "_iff1", th RS notE);
+  PureThy.put_name_hint (PureThy.get_name_hint th ^ "_iff1") (th RS notE);
       
 fun add_rules simps case_thms size_thms rec_thms inject distinct
                   weak_case_congs cong_att =

--- a/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -128,7 +128,7 @@
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
 
-    val ind_name = Thm.name_of_thm induction;
+    val ind_name = Thm.get_name induction;
     val vs = map (fn i => List.nth (pnames, i)) is;
     val (thm', thy') = thy
       |> Theory.absolute_path
@@ -196,7 +196,7 @@
             [asm_simp_tac (HOL_basic_ss addsimps case_rewrites),
              resolve_tac prems, asm_simp_tac HOL_basic_ss])]);
 
-    val exh_name = Thm.name_of_thm exhaustion;
+    val exh_name = Thm.get_name exhaustion;
     val (thm', thy') = thy
       |> Theory.absolute_path
       |> PureThy.store_thm ((exh_name ^ "_P_correctness", thm), [])

--- a/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -59,7 +59,7 @@
     val (Const (s, _), ts) = strip_comb S;
     val params = map dest_Var ts;
     val tname = space_implode "_" (Sign.base_name s ^ "T" :: vs);
-    fun constr_of_intr intr = (Sign.base_name (Thm.name_of_thm intr),
+    fun constr_of_intr intr = (Sign.base_name (Thm.get_name intr),
       map (Logic.unvarifyT o snd) (rev (Term.add_vars (prop_of intr) []) \\ params) @
         filter_out (equal Extraction.nullT) (map
           (Logic.unvarifyT o Extraction.etype_of thy vs []) (prems_of intr)),
@@ -189,7 +189,7 @@
           in if conclT = Extraction.nullT
             then list_abs_free (map dest_Free xs, HOLogic.unit)
             else list_abs_free (map dest_Free xs, list_comb
-              (Free ("r" ^ Sign.base_name (Thm.name_of_thm intr),
+              (Free ("r" ^ Sign.base_name (Thm.get_name intr),
                 map fastype_of (rev args) ---> conclT), rev args))
           end
 
@@ -226,7 +226,7 @@
     let
       val r = foldr1 HOLogic.mk_prod rlzs;
       val x = Free ("x", Extraction.etype_of thy vs [] (hd (prems_of induct)));
-      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.name_of_thm intr);
+      fun name_of_fn intr = "r" ^ Sign.base_name (Thm.get_name intr);
       val r' = list_abs_free (List.mapPartial (fn intr =>
         Option.map (pair (name_of_fn intr)) (AList.lookup (op =) frees (name_of_fn intr))) intrs,
           if length concls = 1 then r $ x else r)
@@ -271,7 +271,7 @@
           else forall_intr_prf (Var (hd rs), AbsP ("H", SOME rprem,
             mk_prf (tl rs) prems prf));
 
-  in (Thm.name_of_thm rule, (vs,
+  in (Thm.get_name rule, (vs,
     if rt = Extraction.nullt then rt else
       foldr (uncurry lambda) rt vs1,
     foldr forall_intr_prf (mk_prf rs prems (Proofterm.proof_combP
@@ -349,11 +349,11 @@
     val (thy3', ind_info) = thy2 |>
       OldInductivePackage.add_inductive_i false true "" false false false
         (map Logic.unvarify rlzsets) (map (fn (rintr, intr) =>
-          ((Sign.base_name (Thm.name_of_thm intr), strip_all
+          ((Sign.base_name (Thm.get_name intr), strip_all
             (Logic.unvarify rintr)), [])) (rintrs ~~ intrs)) [] |>>
       Theory.absolute_path;
     val thy3 = PureThy.hide_thms false
-      (map Thm.name_of_thm (#intrs ind_info)) thy3';
+      (map Thm.get_name (#intrs ind_info)) thy3';
 
     (** realizer for induction rule **)
 
@@ -379,7 +379,7 @@
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.name_of_thm induct :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (Thm.get_name induct :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) params' ((induct, thm'), r)] thy'
@@ -427,7 +427,7 @@
            REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (Thm.name_of_thm elim :: vs @ Ps @ ["correctness"]), thm), []) thy
+          (Thm.get_name elim :: vs @ Ps @ ["correctness"]), thm), []) thy
       in
         Extraction.add_realizers_i
           [mk_realizer thy' (vs @ Ps) params' ((elim, thm'), r)] thy'

--- a/src/HOL/Tools/meson.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/meson.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -390,8 +390,7 @@
 (*Use "theorem naming" to label the clauses*)
 fun name_thms label =
     let fun name1 (th, (k,ths)) =
-	  (k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
-
+	  (k-1, PureThy.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/res_axioms.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -518,17 +518,17 @@
                         cls)
  );
 
-fun pairname th = (Thm.name_of_thm th, th);
+fun pairname th = (PureThy.get_name_hint th, th);
 
 (*Principally for debugging*)
 fun cnf_name s = 
   let val th = thm s
-  in cnf_axiom (Thm.name_of_thm th, th) end;
+  in cnf_axiom (PureThy.get_name_hint th, th) end;
 
 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
 
 (*Preserve the name of "th" after the transformation "f"*)
-fun preserve_name f th = Thm.name_thm (Thm.name_of_thm th, f th);
+fun preserve_name f th = PureThy.put_name_hint (PureThy.get_name_hint th) (f th);
 
 fun rules_of_claset cs =
   let val {safeIs,safeEs,hazIs,hazEs,...} = rep_cs cs
@@ -601,7 +601,7 @@
 (*** meson proof methods ***)
 
 fun skolem_use_cache_thm th =
-  case Symtab.lookup (!clause_cache) (Thm.name_of_thm th) of
+  case Symtab.lookup (!clause_cache) (PureThy.get_name_hint th) of
       NONE => skolem_thm th
     | SOME (th',cls) =>
         if eq_thm(th,th') then cls else skolem_thm th;
@@ -631,7 +631,7 @@
   | conj_rule ths = foldr1 conj2_rule ths;
 
 fun skolem_attr (Context.Theory thy, th) =
-      let val name = Thm.name_of_thm th
+      let val name = PureThy.get_name_hint th
           val (cls, thy') = skolem_cache_thm (name, th) thy
       in (Context.Theory thy', conj_rule cls) end
   | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));

--- a/src/HOL/Tools/rewrite_hol_proof.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/HOL/Tools/rewrite_hol_proof.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -286,9 +286,9 @@
 
 (** Replace congruence rules by substitution rules **)
 
-fun strip_cong ps (PThm (("HOL.cong", _), _, _, _) % _ % _ % SOME x % SOME y %%
+fun strip_cong ps (PThm ("HOL.cong", _, _, _) % _ % _ % SOME x % SOME y %%
       prf1 %% prf2) = strip_cong (((x, y), prf2) :: ps) prf1
-  | strip_cong ps (PThm (("HOL.refl", _), _, _, _) % SOME f) = SOME (f, ps)
+  | strip_cong ps (PThm ("HOL.refl", _, _, _) % SOME f) = SOME (f, ps)
   | strip_cong _ _ = NONE;
 
 val subst_prf = fst (strip_combt (#2 (#der (rep_thm subst))));
@@ -310,15 +310,15 @@
 
 fun mk_AbsP P t = AbsP ("H", P, t);
 
-fun elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % _ % _ %% prf1 %% prf2) =
+fun elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 []) (strip_cong [] prf1)
-  | elim_cong Ts (PThm (("HOL.iffD1", _), _, _, _) % P % _ %% prf) =
+  | elim_cong Ts (PThm ("HOL.iffD1", _, _, _) % P % _ %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [])
         (strip_cong [] (incr_pboundvars 1 0 prf))
-  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % _ %% prf1 %% prf2) =
+  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % _ %% prf1 %% prf2) =
       Option.map (make_subst Ts prf2 [] o
         apsnd (map (make_sym Ts))) (strip_cong [] prf1)
-  | elim_cong Ts (PThm (("HOL.iffD2", _), _, _, _) % _ % P %% prf) =
+  | elim_cong Ts (PThm ("HOL.iffD2", _, _, _) % _ % P %% prf) =
       Option.map (mk_AbsP P o make_subst Ts (PBound 0) [] o
         apsnd (map (make_sym Ts))) (strip_cong [] (incr_pboundvars 1 0 prf))
   | elim_cong _ _ = NONE;

--- a/src/Provers/clasimp.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Provers/clasimp.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -115,8 +115,8 @@
                             CHANGED o Simplifier.asm_lr_simp_tac ss));
 
 (*Attach a suffix, provided we have a name to start with.*)
-fun suffix_thm "" _ th = th
-  | suffix_thm a b th = Thm.name_thm (a^b, th);
+fun suffix_thm "" _ = I
+  | suffix_thm a b = PureThy.put_name_hint (a^b);
 
 (* iffs: addition of rules to simpsets and clasets simultaneously *)
 
@@ -129,7 +129,7 @@
 
 fun addIff decls1 decls2 simp ((cs, ss), th) =
   let
-    val name = Thm.name_of_thm th;
+    val name = PureThy.get_name_hint th;
     val n = nprems_of th;
     val (elim, intro) = if n = 0 then decls1 else decls2;
     val zero_rotate = zero_var_indexes o rotate_prems n;

--- a/src/Provers/classical.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Provers/classical.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -195,7 +195,7 @@
           else all_tac))
         |> Seq.hd
         |> Drule.zero_var_indexes
-        |> Thm.put_name_tags (Thm.get_name_tags rule);
+        |> PureThy.put_name_hint (PureThy.get_name_hint rule);
     in if Drule.equiv_thm (rule, rule'') then rule else rule'' end
   else rule;
 
@@ -424,9 +424,9 @@
     if has_fewer_prems 1 th then
     	error("Ill-formed destruction rule\n" ^ string_of_thm th)
     else
-    case Thm.name_of_thm th of
+    case PureThy.get_name_hint th of
         "" => Tactic.make_elim th
-      | a  => Thm.name_thm (a ^ "_dest", Tactic.make_elim th);
+      | a  => PureThy.put_name_hint (a ^ "_dest") (Tactic.make_elim th);
 
 fun cs addSDs ths = cs addSEs (map name_make_elim ths);
 

--- a/src/Pure/Isar/element.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Isar/element.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -226,7 +226,7 @@
 
 fun thm_name kind th prts =
   let val head =
-    (case #1 (Thm.get_name_tags th) of
+    (case PureThy.get_name_hint th of
       "" => Pretty.command kind
     | a => Pretty.block [Pretty.command kind, Pretty.brk 1, Pretty.str (Sign.base_name a ^ ":")])
   in Pretty.block (Pretty.fbreaks (head :: prts)) end;

--- a/src/Pure/Isar/rule_cases.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -215,7 +215,7 @@
 
 fun lookup_consumes th =
   let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in
-    (case AList.lookup (op =) (Thm.tags_of_thm th) (consumes_tagN) of
+    (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of
       NONE => NONE
     | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ())
     | _ => err ())
@@ -249,7 +249,7 @@
       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;
+fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN;
 
 val save_case_names = add_case_names o lookup_case_names;
 val name = add_case_names o SOME;
@@ -264,16 +264,16 @@
 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) = PureThy.map_tags (fn tags =>
+fun add_case_concl (name, cs) = Thm.map_tags (fn tags =>
   filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]);
 
 fun get_case_concls th name =
-  (case find_first (is_case_concl name) (Thm.tags_of_thm th) of
+  (case find_first (is_case_concl name) (Thm.get_tags th) of
     SOME (_, _ :: cs) => cs
   | _ => []);
 
 fun save_case_concls th =
-  let val concls = Thm.tags_of_thm th |> map_filter
+  let val concls = Thm.get_tags th |> map_filter
     (fn (a, b :: cs) =>
       if a = case_concl_tagN then SOME (b, cs) else NONE
     | _ => NONE)

--- a/src/Pure/Proof/extraction.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Proof/extraction.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -314,7 +314,7 @@
     val rd = ProofSyntax.read_proof thy' false
   in fn (thm, (vs, s1, s2)) =>
     let
-      val name = Thm.name_of_thm thm;
+      val name = Thm.get_name thm;
       val _ = assert (name <> "") "add_realizers: unnamed theorem";
       val prop = Pattern.rewrite_term thy'
         (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
@@ -359,7 +359,7 @@
     val {realizes_eqns, typeof_eqns, types, realizers,
       defs, expand, prep} = ExtractionData.get thy;
 
-    val name = Thm.name_of_thm thm;
+    val name = Thm.get_name thm;
     val _ = assert (name <> "") "add_expand_thms: unnamed theorem";
 
     val is_def =
@@ -555,7 +555,7 @@
               (defs3, corr_prf1 % u %% corr_prf2)
           end
 
-      | corr d defs vs ts Ts hs (prf0 as PThm ((name, _), prf, prop, SOME Ts')) _ _ =
+      | corr d defs vs ts Ts hs (prf0 as PThm (name, prf, prop, SOME Ts')) _ _ =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye;
@@ -578,7 +578,7 @@
                     val corr_prop = Reconstruct.prop_of corr_prf;
                     val corr_prf' = foldr forall_intr_prf
                       (proof_combt
-                         (PThm ((corr_name name vs', []), corr_prf, corr_prop,
+                         (PThm (corr_name name vs', corr_prf, corr_prop,
                              SOME (map TVar (term_tvars corr_prop))), vfs_of corr_prop))
 		      (map (get_var_type corr_prop) (vfs_of prop))
                   in
@@ -643,7 +643,7 @@
               in (defs'', f $ t) end
           end
 
-      | extr d defs vs ts Ts hs (prf0 as PThm ((s, _), prf, prop, SOME Ts')) =
+      | extr d defs vs ts Ts hs (prf0 as PThm (s, prf, prop, SOME Ts')) =
           let
             val (vs', tye) = find_inst prop Ts ts vs;
             val tye' = (map fst (term_tvars prop) ~~ Ts') @ tye
@@ -687,7 +687,7 @@
                     val corr_prop = Reconstruct.prop_of corr_prf';
                     val corr_prf'' = foldr forall_intr_prf
                       (proof_combt
-                        (PThm ((corr_name s vs', []), corr_prf', corr_prop,
+                        (PThm (corr_name s vs', corr_prf', corr_prop,
                           SOME (map TVar (term_tvars corr_prop))),  vfs_of corr_prop))
 		      (map (get_var_type corr_prop) (vfs_of prop));
                   in
@@ -719,7 +719,7 @@
     fun prep_thm (thm, vs) =
       let
         val {prop, der = (_, prf), sign, ...} = rep_thm thm;
-        val name = Thm.name_of_thm thm;
+        val name = Thm.get_name thm;
         val _ = assert (name <> "") "extraction: unnamed theorem";
         val _ = assert (etype_of thy' vs [] prop <> nullT) ("theorem " ^
           quote name ^ " has no computational content")

--- a/src/Pure/Proof/proof_rewrite_rules.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -32,12 +32,12 @@
     val equal_elim_axm = ax equal_elim_axm [];
     val symmetric_axm = ax symmetric_axm [propT];
 
-    fun rew' (PThm (("ProtoPure.protectD", _), _, _, _) % _ %%
-        (PThm (("ProtoPure.protectI", _), _, _, _) % _ %% prf)) = SOME prf
-      | rew' (PThm (("ProtoPure.conjunctionD1", _), _, _, _) % _ % _ %%
-        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% prf %% _)) = SOME prf
-      | rew' (PThm (("ProtoPure.conjunctionD2", _), _, _, _) % _ % _ %%
-        (PThm (("ProtoPure.conjunctionI", _), _, _, _) % _ % _ %% _ %% prf)) = SOME prf
+    fun rew' (PThm ("ProtoPure.protectD", _, _, _) % _ %%
+        (PThm ("ProtoPure.protectI", _, _, _) % _ %% prf)) = SOME prf
+      | rew' (PThm ("ProtoPure.conjunctionD1", _, _, _) % _ % _ %%
+        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% prf %% _)) = SOME prf
+      | rew' (PThm ("ProtoPure.conjunctionD2", _, _, _) % _ % _ %%
+        (PThm ("ProtoPure.conjunctionI", _, _, _) % _ % _ %% _ %% prf)) = SOME prf
       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % _ % _ %%
         (PAxm ("ProtoPure.equal_intr", _, _) % _ % _ %% prf %% _)) = SOME prf
       | rew' (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
@@ -47,14 +47,14 @@
       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
           _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1) %%
-        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %% prf1 %% prf2))
 
       | rew' (PAxm ("ProtoPure.equal_elim", _, _) % SOME (_ $ A) % SOME (_ $ B) %%
         (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %%
           (PAxm ("ProtoPure.combination", _, _) % SOME (Const ("prop", _)) %
              _ % _ % _ %% (PAxm ("ProtoPure.reflexive", _, _) % _) %% prf1)) %%
-        ((tg as PThm (("ProtoPure.protectI", _), _, _, _)) % _ %% prf2)) =
+        ((tg as PThm ("ProtoPure.protectI", _, _, _)) % _ %% prf2)) =
         SOME (tg %> B %% (equal_elim_axm %> A %> B %%
           (symmetric_axm % ?? B % ?? A %% prf1) %% prf2))
 
@@ -222,7 +222,7 @@
   | insert_refl defs Ts (AbsP (s, t, prf)) =
       AbsP (s, t, insert_refl defs Ts prf)
   | insert_refl defs Ts prf = (case strip_combt prf of
-        (PThm ((s, _), _, prop, SOME Ts), ts) =>
+        (PThm (s, _, prop, SOME Ts), ts) =>
           if member (op =) defs s then
             let
               val vs = vars_of prop;
@@ -241,7 +241,7 @@
 fun elim_defs thy r defs prf =
   let
     val defs' = map (Logic.dest_equals o prop_of o Drule.abs_def) defs
-    val defnames = map Thm.name_of_thm defs;
+    val defnames = map Thm.get_name defs;
     val f = if not r then I else
       let
         val cnames = map (fst o dest_Const o fst) defs';

--- a/src/Pure/Proof/proof_syntax.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -108,12 +108,12 @@
       | rename (AbsP (s, t, prf)) = AbsP (s, t, rename prf)
       | rename (prf1 %% prf2) = rename prf1 %% rename prf2
       | rename (prf % t) = rename prf % t
-      | rename (prf' as PThm ((s, tags), prf, prop, Ts)) =
+      | rename (prf' as PThm (s, prf, prop, Ts)) =
           let
             val prop' = the_default (Bound 0) (AList.lookup (op =) thms' s);
             val ps = remove (op =) prop' (map fst (the (Symtab.lookup thms s)))
           in if prop = prop' then prf' else
-            PThm ((s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps), tags),
+            PThm (s ^ "_" ^ string_of_int (length ps - find_index (fn p => p = prop) ps),
               prf, prop, Ts)
           end
       | rename prf = prf
@@ -183,9 +183,9 @@
 val mk_tyapp = fold (fn T => fn prf => Const ("Appt",
   [proofT, Term.itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
 
-fun term_of _ (PThm ((name, _), _, _, NONE)) =
+fun term_of _ (PThm (name, _, _, NONE)) =
       Const (NameSpace.append "thm" name, proofT)
-  | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
+  | term_of _ (PThm (name, _, _, SOME Ts)) =
       mk_tyapp Ts (Const (NameSpace.append "thm" name, proofT))
   | term_of _ (PAxm (name, _, NONE)) = Const (NameSpace.append "axm" name, proofT)
   | term_of _ (PAxm (name, _, SOME Ts)) =

--- a/src/Pure/Proof/proofchecker.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Proof/proofchecker.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -45,7 +45,7 @@
         Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
       end;
 
-    fun thm_of _ _ (PThm ((name, _), _, prop', SOME Ts)) =
+    fun thm_of _ _ (PThm (name, _, prop', SOME Ts)) =
           let
             val thm = Drule.implies_intr_hyps (lookup name);
             val {prop, ...} = rep_thm thm;

--- a/src/Pure/Proof/reconstruct.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Proof/reconstruct.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -151,7 +151,7 @@
             val prop'' = subst_TVars (map fst tvars @ map snd fmap ~~ Ts)
               (forall_intr_vfs prop') handle Library.UnequalLengths =>
                 error ("Wrong number of type arguments for " ^
-                  quote (fst (get_name_tags [] prop prf)))
+                  quote (get_name [] prop prf))
           in (prop'', change_type (SOME Ts) prf, [], env', vTs) end;
 
     fun head_norm (prop, prf, cnstrts, env, vTs) =
@@ -352,7 +352,7 @@
       | expand maxidx prfs (prf % t) =
           let val (maxidx', prfs', prf') = expand maxidx prfs prf
           in (maxidx', prfs', prf' % t) end
-      | expand maxidx prfs (prf as PThm ((a, _), cprf, prop, SOME Ts)) =
+      | expand maxidx prfs (prf as PThm (a, cprf, prop, SOME Ts)) =
           if not (exists
             (fn (b, NONE) => a = b
               | (b, SOME prop') => a = b andalso prop = prop') thms)

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -338,7 +338,7 @@
 (* FIXME: check this uses non-transitive closure function here *)
 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   let
-    val names = filter_out (equal "") (map Thm.name_of_thm ths);
+    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
     val deps = filter_out (equal "")
       (Symtab.keys (fold Proofterm.thms_of_proof
         (map Thm.proof_of ths) Symtab.empty));

--- a/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -25,9 +25,9 @@
 fun enable () = if ! proofs = 0 then proofs := 1 else ();
 fun disable () = proofs := 0;
 
-fun dest_thm_axm (PThm (nt, prf, _, _)) = (nt, prf)
-  | dest_thm_axm (PAxm (n, _, _)) = ((n ^ " (Ax)", []), MinProof ([], [], []))
-  | dest_thm_axm _ = (("", []), MinProof ([], [], []));
+fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
+  | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
+  | dest_thm_axm _ = ("", MinProof ([], [], []));
 
 fun make_deps_graph (AbsP (_, _, prf)) = make_deps_graph prf
   | make_deps_graph (Abst (_, _, prf)) = make_deps_graph prf
@@ -37,9 +37,9 @@
       fold (make_deps_graph o Proofterm.proof_of_min_thm) thms #>
       fold (make_deps_graph o Proofterm.proof_of_min_axm) axms
   | make_deps_graph prf = (fn p as (gra, parents) =>
-      let val ((name, tags), prf') = dest_thm_axm prf
+      let val (name, prf') = dest_thm_axm prf
       in
-        if name <> "" andalso not (PureThy.has_internal tags) then
+        if name <> "" then
           if not (Symtab.defined gra name) then
             let
               val (gra', parents') = make_deps_graph prf' (gra, []);

--- a/src/Pure/display.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/display.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -77,7 +77,7 @@
     val th = Thm.strip_shyps raw_th;
     val {hyps, tpairs, prop, der = (ora, _), ...} = Thm.rep_thm th;
     val xshyps = Thm.extra_shyps th;
-    val (_, tags) = Thm.get_name_tags th;
+    val tags = Thm.get_tags th;
 
     val q = if quote then Pretty.quote else I;
     val prt_term = q o (Pretty.term pp);

--- a/src/Pure/drule.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/drule.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -427,7 +427,7 @@
     |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
 
 fun close_derivation thm =
-  if Thm.get_name_tags thm = ("", []) then Thm.name_thm ("", thm)
+  if Thm.get_name thm = "" then Thm.put_name "" thm
   else thm;
 
 

--- a/src/Pure/meta_simplifier.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/meta_simplifier.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -514,7 +514,7 @@
   end;
 
 fun extract_rews (Simpset (_, {mk_rews = {mk, ...}, ...}), thms) =
-  maps (fn thm => map (rpair (Thm.name_of_thm thm)) (mk thm)) thms;
+  maps (fn thm => map (rpair (PureThy.get_name_hint thm)) (mk thm)) thms;
 
 fun extract_safe_rrules (ss, thm) =
   maps (orient_rrule ss) (extract_rews (ss, [thm]));

--- a/src/Pure/proof_general.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/proof_general.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -481,7 +481,7 @@
 (* FIXME: check this uses non-transitive closure function here *)
 fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
   let
-    val names = filter_out (equal "") (map Thm.name_of_thm ths);
+    val names = filter_out (equal "") (map PureThy.get_name_hint ths);
     val deps = filter_out (equal "")
       (Symtab.keys (fold Proofterm.thms_of_proof
         (map Thm.proof_of ths) Symtab.empty));

--- a/src/Pure/proofterm.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/proofterm.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -18,7 +18,7 @@
    | % of proof * term option
    | %% of proof * proof
    | Hyp of term
-   | PThm of (string * (string * string list) list) * proof * term * typ list option
+   | PThm of string * proof * term * typ list option
    | PAxm of string * term * typ list option
    | Oracle of string * term * typ list option
    | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
@@ -99,9 +99,8 @@
   val equal_elim : term -> term -> proof -> proof -> proof
   val axm_proof : string -> term -> proof
   val oracle_proof : string -> term -> proof
-  val thm_proof : theory -> string * (string * string list) list ->
-    term list -> term -> proof -> proof
-  val get_name_tags : term list -> term -> proof -> string * (string * string list) list
+  val thm_proof : theory -> string -> term list -> term -> proof -> proof
+  val get_name : term list -> term -> proof -> string
 
   (** rewriting on proof terms **)
   val add_prf_rrules : (proof * proof) list -> theory -> theory
@@ -112,7 +111,7 @@
   val rewrite_proof_notypes : (proof * proof) list *
     (string * (typ list -> proof -> proof option)) list -> proof -> proof
   val init_data: theory -> theory
-  
+
 end
 
 structure Proofterm : PROOFTERM =
@@ -127,13 +126,13 @@
  | op % of proof * term option
  | op %% of proof * proof
  | Hyp of term
- | PThm of (string * (string * string list) list) * proof * term * typ list option
+ | PThm of string * proof * term * typ list option
  | PAxm of string * term * typ list option
  | Oracle of string * term * typ list option
  | MinProof of ((string * term) * proof) list * (string * term) list * (string * term) list;
 
 fun proof_of_min_axm (s, prop) = PAxm (s, prop, NONE);
-fun proof_of_min_thm ((s, prop), prf) = PThm ((s, []), prf, prop, NONE);
+fun proof_of_min_thm ((s, prop), prf) = PThm (s, prf, prop, NONE);
 
 val string_term_ord = prod_ord fast_string_ord Term.fast_term_ord;
 
@@ -143,7 +142,7 @@
       | oras_of (AbsP (_, _, prf)) = oras_of prf
       | oras_of (prf % _) = oras_of prf
       | oras_of (prf1 %% prf2) = oras_of prf1 #> oras_of prf2
-      | oras_of (PThm ((name, _), prf, prop, _)) = (fn tabs as (thms, oras) =>
+      | oras_of (PThm (name, prf, prop, _)) = (fn tabs as (thms, oras) =>
           case Symtab.lookup thms name of
             NONE => oras_of prf (Symtab.update (name, [prop]) thms, oras)
           | SOME ps => if member (op =) ps prop then tabs else
@@ -162,7 +161,7 @@
   | thms_of_proof (AbsP (_, _, prf)) = thms_of_proof prf
   | thms_of_proof (prf1 %% prf2) = thms_of_proof prf1 #> thms_of_proof prf2
   | thms_of_proof (prf % _) = thms_of_proof prf
-  | thms_of_proof (prf' as PThm ((s, _), prf, prop, _)) = (fn tab =>
+  | thms_of_proof (prf' as PThm (s, prf, prop, _)) = (fn tab =>
       case Symtab.lookup tab s of
         NONE => thms_of_proof prf (Symtab.update (s, [(prop, prf')]) tab)
       | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
@@ -175,8 +174,8 @@
   | thms_of_proof' (AbsP (_, _, prf)) = thms_of_proof' prf
   | thms_of_proof' (prf1 %% prf2) = thms_of_proof' prf1 #> thms_of_proof' prf2
   | thms_of_proof' (prf % _) = thms_of_proof' prf
-  | thms_of_proof' (PThm (("", _), prf, prop, _)) = thms_of_proof' prf
-  | thms_of_proof' (prf' as PThm ((s, _), _, prop, _)) = (fn tab =>
+  | thms_of_proof' (PThm ("", prf, prop, _)) = thms_of_proof' prf
+  | thms_of_proof' (prf' as PThm (s, _, prop, _)) = (fn tab =>
       case Symtab.lookup tab s of
         NONE => Symtab.update (s, [(prop, prf')]) tab
       | SOME ps => if exists (fn (p, _) => p = prop) ps then tab else
@@ -200,7 +199,7 @@
   | mk_min_proof (AbsP (_, _, prf)) = mk_min_proof prf
   | mk_min_proof (prf % _) = mk_min_proof prf
   | mk_min_proof (prf1 %% prf2) = mk_min_proof prf1 #> mk_min_proof prf2
-  | mk_min_proof (PThm ((s, _), prf, prop, _)) =
+  | mk_min_proof (PThm (s, prf, prop, _)) =
       map3 (OrdList.insert (string_term_ord o pairself fst) ((s, prop), prf)) I I
   | mk_min_proof (PAxm (s, prop, _)) =
       map3 I (OrdList.insert string_term_ord (s, prop)) I
@@ -239,12 +238,12 @@
 val proof_combt' = Library.foldl (op %);
 val proof_combP = Library.foldl (op %%);
 
-fun strip_combt prf = 
+fun strip_combt prf =
     let fun stripc (prf % t, ts) = stripc (prf, t::ts)
-          | stripc  x =  x 
+          | stripc  x =  x
     in  stripc (prf, [])  end;
 
-fun strip_combP prf = 
+fun strip_combP prf =
     let fun stripc (prf %% prf', prfs) = stripc (prf, prf'::prfs)
           | stripc  x =  x
     in  stripc (prf, [])  end;
@@ -330,7 +329,7 @@
 fun mk_abs Ts t = Library.foldl (fn (t', T) => Abs ("", T, t')) (t, Ts);
 
 
-(*Abstraction of a proof term over its occurrences of v, 
+(*Abstraction of a proof term over its occurrences of v,
     which must contain no loose bound variables.
   The resulting proof term is ready to become the body of an Abst.*)
 
@@ -365,17 +364,17 @@
 fun incr_bv' inct tlev t = incr_bv (inct, tlev, t);
 
 fun prf_incr_bv' incP inct Plev tlev (PBound i) =
-      if i >= Plev then PBound (i+incP) else raise SAME 
+      if i >= Plev then PBound (i+incP) else raise SAME
   | prf_incr_bv' incP inct Plev tlev (AbsP (a, t, body)) =
       (AbsP (a, apsome' (same (incr_bv' inct tlev)) t,
          prf_incr_bv incP inct (Plev+1) tlev body) handle SAME =>
            AbsP (a, t, prf_incr_bv' incP inct (Plev+1) tlev body))
   | prf_incr_bv' incP inct Plev tlev (Abst (a, T, body)) =
       Abst (a, T, prf_incr_bv' incP inct Plev (tlev+1) body)
-  | prf_incr_bv' incP inct Plev tlev (prf %% prf') = 
+  | prf_incr_bv' incP inct Plev tlev (prf %% prf') =
       (prf_incr_bv' incP inct Plev tlev prf %% prf_incr_bv incP inct Plev tlev prf'
        handle SAME => prf %% prf_incr_bv' incP inct Plev tlev prf')
-  | prf_incr_bv' incP inct Plev tlev (prf % t) = 
+  | prf_incr_bv' incP inct Plev tlev (prf % t) =
       (prf_incr_bv' incP inct Plev tlev prf % Option.map (incr_bv' inct tlev) t
        handle SAME => prf % apsome' (same (incr_bv' inct tlev)) t)
   | prf_incr_bv' _ _ _ _ _ = raise SAME
@@ -539,7 +538,7 @@
   | thaw names names' (Abs (s, T, t)) =
       Abs (s, thawT names' T, thaw names names' t)
   | thaw names names' (Const (s, T)) = Const (s, thawT names' T)
-  | thaw names names' (Free (s, T)) = 
+  | thaw names names' (Free (s, T)) =
       let val T' = thawT names' T
       in case AList.lookup (op =) names s of
           NONE => Free (s, T')
@@ -703,12 +702,12 @@
     val ps = map (Logic.lift_all inc Bi) (Logic.strip_imp_prems prop);
     val k = length ps;
 
-    fun mk_app (b, (i, j, prf)) = 
+    fun mk_app (b, (i, j, prf)) =
           if b then (i-1, j, prf %% PBound i) else (i, j-1, prf %> Bound j);
 
     fun lift Us bs i j (Const ("==>", _) $ A $ B) =
             AbsP ("H", NONE (*A*), lift Us (true::bs) (i+1) j B)
-      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) = 
+      | lift Us bs i j (Const ("all", _) $ Abs (a, T, t)) =
             Abst (a, NONE (*T*), lift (T::Us) (false::bs) i (j+1) t)
       | lift Us bs i j _ = proof_combP (lifth' (rev Us) [] prf,
             map (fn k => (#3 (foldr mk_app (i-1, j-1, PBound k) bs)))
@@ -888,7 +887,7 @@
       | t' => is_p 0 t')
   end;
 
-fun needed_vars prop = 
+fun needed_vars prop =
   Library.foldl (op union)
     ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
   prop_vars prop;
@@ -915,7 +914,7 @@
   let
     val compress_typ = Compress.typ thy;
     val compress_term = Compress.term thy;
-  
+
     fun shrink ls lev (prf as Abst (a, T, body)) =
           let val (b, is, ch, body') = shrink ls (lev+1) body
           in (b, is, ch, if ch then Abst (a, Option.map compress_typ T, body') else prf) end
@@ -1029,8 +1028,7 @@
           mtch Ts (i+1) j (optmatch (matcht Ts j) inst (opt, opu)) (prf1, prf2)
       | mtch Ts i j inst (prf1, AbsP (_, _, prf2)) =
           mtch Ts (i+1) j inst (incr_pboundvars 1 0 prf1 %% PBound 0, prf2)
-      | mtch Ts i j inst (PThm ((name1, _), _, prop1, opTs),
-            PThm ((name2, _), _, prop2, opUs)) =
+      | mtch Ts i j inst (PThm (name1, _, prop1, opTs), PThm (name2, _, prop2, opUs)) =
           if name1=name2 andalso prop1=prop2 then
             optmatch matchTs inst (opTs, opUs)
           else raise PMatch
@@ -1070,7 +1068,7 @@
       | subst _ _ t = t
   in subst 0 0 end;
 
-(*A fast unification filter: true unless the two terms cannot be unified. 
+(*A fast unification filter: true unless the two terms cannot be unified.
   Terms must be NORMAL.  Treats all Vars as distinct. *)
 fun could_unify prf1 prf2 =
   let
@@ -1088,7 +1086,7 @@
   in case (head_of prf1, head_of prf2) of
         (_, Hyp (Var _)) => true
       | (Hyp (Var _), _) => true
-      | (PThm ((a, _), _, propa, _), PThm ((b, _), _, propb, _)) =>
+      | (PThm (a, _, propa, _), PThm (b, _, propb, _)) =>
           a = b andalso propa = propb andalso matchrands prf1 prf2
       | (PAxm (a, _, _), PAxm (b, _, _)) => a = b andalso matchrands prf1 prf2
       | (PBound i, PBound j) =>  i = j andalso matchrands prf1 prf2
@@ -1203,7 +1201,7 @@
   let val r = ProofData.get thy
   in ProofData.put (fst r, ps @ snd r) thy end;
 
-fun thm_proof thy (name, tags) hyps prop prf =
+fun thm_proof thy name hyps prop prf =
   let
     val prop = Logic.list_implies (hyps, prop);
     val nvs = needed_vars prop;
@@ -1215,25 +1213,23 @@
           (foldr (uncurry implies_intr_proof) prf hyps)))
       else MinProof (mk_min_proof prf ([], [], []));
     val head = (case strip_combt (fst (strip_combP prf)) of
-        (PThm ((old_name, _), prf', prop', NONE), args') =>
+        (PThm (old_name, prf', prop', NONE), args') =>
           if (old_name="" orelse old_name=name) andalso
              prop = prop' andalso args = args' then
-            PThm ((name, tags), prf', prop, NONE)
+            PThm (name, prf', prop, NONE)
           else
-            PThm ((name, tags), opt_prf, prop, NONE)
-      | _ => PThm ((name, tags), opt_prf, prop, NONE))
+            PThm (name, opt_prf, prop, NONE)
+      | _ => PThm (name, opt_prf, prop, NONE))
   in
     proof_combP (proof_combt' (head, args), map Hyp hyps)
   end;
 
-fun get_name_tags hyps prop prf =
+fun get_name hyps prop prf =
   let val prop = Logic.list_implies (hyps, prop) in
     (case strip_combt (fst (strip_combP prf)) of
-      (PThm ((name, tags), _, prop', _), _) =>
-        if prop=prop' then (name, tags) else ("", [])
-    | (PAxm (name, prop', _), _) =>
-        if prop=prop' then (name, []) else ("", [])
-    | _ => ("", []))
+      (PThm (name, _, prop', _), _) => if prop=prop' then name else ""
+    | (PAxm (name, prop', _), _) => if prop=prop' then name else ""
+    | _ => "")
   end;
 
 end;

--- a/src/Pure/pure_thy.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/pure_thy.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -29,11 +29,12 @@
 signature PURE_THY =
 sig
   include BASIC_PURE_THY
-  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_name_hint: thm -> string
+  val put_name_hint: string -> thm -> thm
   val get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
@@ -62,7 +63,9 @@
   val burrow_facts: ('a list -> 'b list) ->
     ('c * ('a list * 'd) list) list -> ('c * ('b list * 'd) list) list
   val name_multi: string -> 'a list -> (string * 'a) list
-  val name_thm: bool -> string * thm -> thm
+  val name_thm: bool -> bool -> string -> thm -> thm
+  val name_thms: bool -> bool -> string -> thm list -> thm list
+  val name_thmss: bool -> string -> (thm list * 'a) list -> (thm list * 'a) list
   val store_thm: (bstring * thm) * attribute list -> theory -> thm * theory
   val smart_store_thms: (bstring * thm list) -> thm list
   val smart_store_thms_open: (bstring * thm list) -> thm list
@@ -106,12 +109,8 @@
 
 (* add / delete tags *)
 
-fun map_tags f thm =
-  let val (name, tags) = Thm.get_name_tags thm
-  in Thm.put_name_tags (name, f tags) thm end;
-
-fun tag_rule tg = map_tags (fn tgs => if member (op =) tgs tg then tgs else tgs @ [tg]);
-fun untag_rule s = map_tags (filter_out (fn (s', _) => s = s'));
+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;
@@ -119,18 +118,28 @@
 fun simple_tag name x = tag (name, []) x;
 
 
+(* unofficial theorem names *)
+
+fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]);
+
+fun get_name_hint thm =
+  (case AList.lookup (op =) (Thm.get_tags thm) "name" of
+    SOME (k :: _) => k
+  | _ => "??.unknown");
+
+
 (* theorem kinds *)
 
 fun get_kind thm =
-  (case AList.lookup (op =) ((#2 o Thm.get_name_tags) thm) "kind" of
+  (case AList.lookup (op =) (Thm.get_tags thm) "kind" of
     SOME (k :: _) => k
-  | _ => "unknown");
+  | _ => "??.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;
+val is_internal = has_internal o Thm.get_tags;
 
 
 
@@ -288,14 +297,14 @@
 
 fun thms_containing_consts thy consts =
   thms_containing thy (consts, []) |> maps #2
-  |> map (fn th => (Thm.name_of_thm th, th));
+  |> map (`(get_name_hint));
 
 
 (* thms_of etc. *)
 
 fun thms_of thy =
   let val thms = #2 (theorems_of thy)
-  in map (fn th => (Thm.name_of_thm th, th)) (maps snd (Symtab.dest thms)) end;
+  in map (`(get_name_hint)) (maps snd (Symtab.dest thms)) end;
 
 fun all_thms_of thy = maps thms_of (thy :: Theory.ancestors_of thy);
 
@@ -327,12 +336,15 @@
 fun name_multi name [x] = [(name, x)]
   | name_multi name xs = gen_names 0 (length xs) name ~~ xs;
 
-fun name_thm pre (name, thm) =
-  if Thm.name_of_thm thm <> "" andalso pre then thm else Thm.name_thm (name, thm);
+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 get_name_hint thm <> "" andalso pre orelse name = "" then I else put_name_hint name);
 
-fun name_thms pre name xs = map (name_thm pre) (name_multi name xs);
+fun name_thms pre official name xs =
+  map (uncurry (name_thm pre official)) (name_multi name xs);
 
-fun name_thmss name fact = burrow_fact (name_thms true name) fact;
+fun name_thmss official name fact =
+  burrow_fact (name_thms true official name) fact;
 
 
 (* enter_thms *)
@@ -363,7 +375,8 @@
 (* add_thms(s) *)
 
 fun add_thms_atts pre_name ((bname, thms), atts) =
-  enter_thms pre_name (name_thms false) (foldl_map (Thm.theory_attributes atts)) (bname, thms);
+  enter_thms pre_name (name_thms false true)
+    (foldl_map (Thm.theory_attributes atts)) (bname, thms);
 
 fun gen_add_thmss pre_name =
   fold_map (add_thms_atts pre_name);
@@ -371,8 +384,8 @@
 fun gen_add_thms pre_name args =
   apfst (map hd) o gen_add_thmss pre_name (map (apfst (apsnd single)) args);
 
-val add_thmss = gen_add_thmss (name_thms true);
-val add_thms = gen_add_thms (name_thms true);
+val add_thmss = gen_add_thmss (name_thms true true);
+val add_thms = gen_add_thms (name_thms true true);
 
 
 (* note_thmss(_i) *)
@@ -383,7 +396,7 @@
   let
     fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths);
     val (thms, thy') = thy |> enter_thms
-      name_thmss (name_thms false) (apsnd flat o foldl_map app)
+      (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app)
       (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts);
   in ((bname, thms), thy') end);
 
@@ -405,7 +418,7 @@
 (* store_thm *)
 
 fun store_thm ((bname, thm), atts) thy =
-  let val ([th'], thy') = add_thms_atts (name_thms true) ((bname, [thm]), atts) thy
+  let val ([th'], thy') = add_thms_atts (name_thms true true) ((bname, [thm]), atts) thy
   in (th', thy') end;
 
 
@@ -415,16 +428,18 @@
 
 fun smart_store _ (name, []) =
       error ("Cannot store empty list of theorems: " ^ quote name)
-  | smart_store name_thm (name, [thm]) =
-      fst (enter_thms (name_thm true) (name_thm false) I (name, [thm]) (Thm.theory_of_thm thm))
-  | smart_store name_thm (name, thms) =
-      let val thy = Theory.merge_list (map Thm.theory_of_thm thms)
-      in fst (enter_thms (name_thm true) (name_thm false) I (name, thms) thy) end;
+  | smart_store official (name, [thm]) =
+      fst (enter_thms (name_thms true official) (name_thms false official) I (name, [thm])
+        (Thm.theory_of_thm thm))
+  | smart_store official (name, thms) =
+      let val thy = Theory.merge_list (map Thm.theory_of_thm thms) in
+        fst (enter_thms (name_thms true official) (name_thms false official) I (name, thms) thy)
+      end;
 
 in
 
-val smart_store_thms = smart_store name_thms;
-val smart_store_thms_open = smart_store (K (K I));
+val smart_store_thms = smart_store true;
+val smart_store_thms_open = smart_store false;
 
 end;
 

--- a/src/Pure/thm.ML	Tue Dec 05 00:29:19 2006 +0100
+++ b/src/Pure/thm.ML	Tue Dec 05 00:30:38 2006 +0100
@@ -55,6 +55,7 @@
    {thy: theory,
     sign: theory,       (*obsolete*)
     der: bool * Proofterm.proof,
+    tags: tag list,
     maxidx: int,
     shyps: sort list,
     hyps: term list,
@@ -64,6 +65,7 @@
    {thy: theory,
     sign: theory,       (*obsolete*)
     der: bool * Proofterm.proof,
+    tags: tag list,
     maxidx: int,
     shyps: sort list,
     hyps: cterm list,
@@ -161,11 +163,10 @@
   val maxidx_thm: thm -> int -> int
   val hyps_of: thm -> term list
   val full_prop_of: thm -> term
-  val get_name_tags: thm -> string * tag list
-  val put_name_tags: string * tag list -> thm -> thm
-  val name_of_thm: thm -> string
-  val tags_of_thm: thm -> tag list
-  val name_thm: string * thm -> thm
+  val get_name: thm -> string
+  val put_name: string -> thm -> thm
+  val get_tags: thm -> tag list
+  val map_tags: (tag list -> tag list) -> thm -> thm
   val compress: thm -> thm
   val adjust_maxidx_thm: int -> thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
@@ -376,17 +377,17 @@
 fun read_cterm thy = #1 o read_def_cterm (thy, K NONE, K NONE) [] true;
 
 
-(*tags provide additional comment, apart from the axiom/theorem name*)
-type tag = string * string list;
-
 
 (*** Meta theorems ***)
 
 structure Pt = Proofterm;
 
+type tag = string * string list;
+
 datatype thm = Thm of
  {thy_ref: theory_ref,         (*dynamic reference to theory*)
   der: bool * Pt.proof,        (*derivation*)
+  tags: tag list,              (*additional annotations/comments*)
   maxidx: int,                 (*maximum index of any Var or TVar*)
   shyps: sort list,            (*sort hypotheses as ordered list*)
   hyps: term list,             (*hypotheses as ordered list*)
@@ -396,19 +397,19 @@
 (*errors involving theorems*)
 exception THM of string * int * thm list;
 
-fun rep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun rep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   let val thy = Theory.deref thy_ref in
-   {thy = thy, sign = thy, der = der, maxidx = maxidx,
+   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx,
     shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop}
   end;
 
 (*version of rep_thm returning cterms instead of terms*)
-fun crep_thm (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun crep_thm (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   let
     val thy = Theory.deref thy_ref;
     fun cterm max t = Cterm {thy_ref = thy_ref, t = t, T = propT, maxidx = max, sorts = shyps};
   in
-   {thy = thy, sign = thy, der = der, maxidx = maxidx, shyps = shyps,
+   {thy = thy, sign = thy, der = der, tags = tags, maxidx = maxidx, shyps = shyps,
     hyps = map (cterm ~1) hyps,
     tpairs = map (pairself (cterm maxidx)) tpairs,
     prop = cterm maxidx prop}
@@ -519,7 +520,7 @@
 (*explicit transfer to a super theory*)
 fun transfer thy' thm =
   let
-    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = thm;
+    val Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop} = thm;
     val thy = Theory.deref thy_ref;
   in
     if not (subthy (thy, thy')) then
@@ -528,6 +529,7 @@
     else
       Thm {thy_ref = Theory.self_ref thy',
         der = der,
+        tags = tags,
         maxidx = maxidx,
         shyps = shyps,
         hyps = hyps,
@@ -539,7 +541,7 @@
 fun weaken raw_ct th =
   let
     val ct as Cterm {t = A, T, sorts, maxidx = maxidxA, ...} = adjust_maxidx_cterm ~1 raw_ct;
-    val Thm {der, maxidx, shyps, hyps, tpairs, prop, ...} = th;
+    val Thm {der, tags, maxidx, shyps, hyps, tpairs, prop, ...} = th;
   in
     if T <> propT then
       raise THM ("weaken: assumptions must have type prop", 0, [])
@@ -548,6 +550,7 @@
     else
       Thm {thy_ref = merge_thys1 ct th,
         der = der,
+        tags = tags,
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = insert_hyps A hyps,
@@ -565,7 +568,7 @@
 
 (*remove extra sorts that are non-empty by virtue of type signature information*)
 fun strip_shyps (thm as Thm {shyps = [], ...}) = thm
-  | strip_shyps (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+  | strip_shyps (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
       let
         val thy = Theory.deref thy_ref;
         val shyps' =
@@ -577,7 +580,7 @@
               val witnessed = map #2 (Sign.witness_sorts thy present extra);
             in Sorts.subtract witnessed shyps end;
       in
-        Thm {thy_ref = thy_ref, der = der, maxidx = maxidx,
+        Thm {thy_ref = thy_ref, der = der, tags = tags, maxidx = maxidx,
           shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}
       end;
 
@@ -596,6 +599,7 @@
       |> Option.map (fn prop =>
           Thm {thy_ref = Theory.self_ref thy,
             der = Pt.infer_derivs' I (false, Pt.axm_proof name prop),
+            tags = [],
             maxidx = maxidx_of_term prop,
             shyps = may_insert_term_sorts thy prop [],
             hyps = [],
@@ -624,30 +628,31 @@
     (Symtab.dest (#2 (#axioms (Theory.rep_theory thy))));
 
 
-(* name and tags -- make proof objects more readable *)
+(* official name and additional tags *)
 
-fun get_name_tags (Thm {hyps, prop, der = (_, prf), ...}) =
-  Pt.get_name_tags hyps prop prf;
+fun get_name (Thm {hyps, prop, der = (_, prf), ...}) =
+  Pt.get_name hyps prop prf;
 
-fun put_name_tags x (Thm {thy_ref, der = (ora, prf), maxidx,
-      shyps, hyps, tpairs = [], prop}) = Thm {thy_ref = thy_ref,
-        der = (ora, Pt.thm_proof (Theory.deref thy_ref) x hyps prop prf),
-        maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
-  | put_name_tags _ thm =
-      raise THM ("put_name_tags: unsolved flex-flex constraints", 0, [thm]);
+fun put_name name (Thm {thy_ref, der = (ora, prf), tags, maxidx, shyps, hyps, tpairs = [], prop}) =
+      Thm {thy_ref = thy_ref,
+        der = (ora, Pt.thm_proof (Theory.deref thy_ref) name hyps prop prf),
+        tags = tags, maxidx = maxidx, shyps = shyps, hyps = hyps, tpairs = [], prop = prop}
+  | put_name _ thm = raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
 
-val name_of_thm = #1 o get_name_tags;
-val tags_of_thm = #2 o get_name_tags;
+val get_tags = #tags o rep_thm;
 
-fun name_thm (name, thm) = put_name_tags (name, tags_of_thm thm) thm;
+fun map_tags f (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
+  Thm {thy_ref = thy_ref, der = der, tags = f tags, maxidx = maxidx,
+    shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
 
 
 (*Compression of theorems -- a separate rule, not integrated with the others,
   as it could be slow.*)
-fun compress (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun compress (Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   let val thy = Theory.deref thy_ref in
     Thm {thy_ref = thy_ref,
       der = der,
+      tags = tags,
       maxidx = maxidx,
       shyps = shyps,
       hyps = map (Compress.term thy) hyps,
@@ -655,14 +660,14 @@
       prop = Compress.term thy prop}
   end;
 
-fun adjust_maxidx_thm i (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun adjust_maxidx_thm i (th as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   if maxidx = i then th
   else if maxidx < i then
-    Thm {maxidx = i, thy_ref = thy_ref, der = der, shyps = shyps,
+    Thm {maxidx = i, thy_ref = thy_ref, der = der, tags = tags, shyps = shyps,
       hyps = hyps, tpairs = tpairs, prop = prop}
   else
-    Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i),
-      thy_ref = thy_ref, der = der, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
+    Thm {maxidx = Int.max (maxidx_tpairs tpairs (maxidx_of_term prop), i), thy_ref = thy_ref,
+      der = der, tags = tags, shyps = shyps, hyps = hyps, tpairs = tpairs, prop = prop};
 
 
 
@@ -679,6 +684,7 @@
       raise THM ("assume: variables", maxidx, [])
     else Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' I (false, Pt.Hyp prop),
+      tags = [],
       maxidx = ~1,
       shyps = sorts,
       hyps = [prop],
@@ -701,6 +707,7 @@
   else
     Thm {thy_ref = merge_thys1 ct th,
       der = Pt.infer_derivs' (Pt.implies_intr_proof A) der,
+      tags = [],
       maxidx = Int.max (maxidxA, maxidx),
       shyps = Sorts.union sorts shyps,
       hyps = remove_hyps A hyps,
@@ -725,6 +732,7 @@
         if A aconv propA then
           Thm {thy_ref = merge_thys2 thAB thA,
             der = Pt.infer_derivs (curry Pt.%%) der derA,
+            tags = [],
             maxidx = Int.max (maxA, maxidx),
             shyps = Sorts.union shypsA shyps,
             hyps = union_hyps hypsA hyps,
@@ -748,6 +756,7 @@
     fun result a =
       Thm {thy_ref = merge_thys1 ct th,
         der = Pt.infer_derivs' (Pt.forall_intr_proof x a) der,
+        tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
@@ -779,6 +788,7 @@
       else
         Thm {thy_ref = merge_thys1 ct th,
           der = Pt.infer_derivs' (Pt.% o rpair (SOME t)) der,
+          tags = [],
           maxidx = Int.max (maxidx, maxt),
           shyps = Sorts.union sorts shyps,
           hyps = hyps,
@@ -795,6 +805,7 @@
 fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
   Thm {thy_ref = thy_ref,
     der = Pt.infer_derivs' I (false, Pt.reflexive),
+    tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
@@ -806,11 +817,12 @@
   ------
   u == t
 *)
-fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun symmetric (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   (case prop of
     (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
       Thm {thy_ref = thy_ref,
         der = Pt.infer_derivs' Pt.symmetric der,
+        tags = [],
         maxidx = maxidx,
         shyps = shyps,
         hyps = hyps,
@@ -837,6 +849,7 @@
         else
           Thm {thy_ref = merge_thys2 th1 th2,
             der = Pt.infer_derivs (Pt.transitive u T) der1 der2,
+            tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
@@ -858,6 +871,7 @@
   in
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' I (false, Pt.reflexive),
+      tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
@@ -868,6 +882,7 @@
 fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
   Thm {thy_ref = thy_ref,
     der = Pt.infer_derivs' I (false, Pt.reflexive),
+    tags = [],
     maxidx = maxidx,
     shyps = sorts,
     hyps = [],
@@ -882,7 +897,7 @@
 *)
 fun abstract_rule a
     (Cterm {t = x, T, sorts, ...})
-    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop}) =
+    (th as Thm {thy_ref, der, maxidx, hyps, shyps, tpairs, prop, ...}) =
   let
     val string_of = Sign.string_of_term (Theory.deref thy_ref);
     val (t, u) = Logic.dest_equals prop
@@ -890,6 +905,7 @@
     val result =
       Thm {thy_ref = thy_ref,
         der = Pt.infer_derivs' (Pt.abstract_rule x a) der,
+        tags = [],
         maxidx = maxidx,
         shyps = Sorts.union sorts shyps,
         hyps = hyps,
@@ -932,6 +948,7 @@
         (chktypes fT tT;
           Thm {thy_ref = merge_thys2 th1 th2,
             der = Pt.infer_derivs (Pt.combination f g t u fT) der1 der2,
+            tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
@@ -958,6 +975,7 @@
         if A aconv A' andalso B aconv B' then
           Thm {thy_ref = merge_thys2 th1 th2,
             der = Pt.infer_derivs (Pt.equal_intr A B) der1 der2,
+            tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
@@ -985,6 +1003,7 @@
         if prop2 aconv A then
           Thm {thy_ref = merge_thys2 th1 th2,
             der = Pt.infer_derivs (Pt.equal_elim A B) der1 der2,
+            tags = [],
             maxidx = Int.max (max1, max2),
             shyps = Sorts.union shyps1 shyps2,
             hyps = union_hyps hyps1 hyps2,
@@ -1002,7 +1021,7 @@
   Instantiates the theorem and deletes trivial tpairs.
   Resulting sequence may contain multiple elements if the tpairs are
     not all flex-flex. *)
-fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun flexflex_rule (th as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   Unify.smash_unifiers (Theory.deref thy_ref) tpairs (Envir.empty maxidx)
   |> Seq.map (fn env =>
       if Envir.is_empty env then th
@@ -1015,6 +1034,7 @@
         in
           Thm {thy_ref = thy_ref,
             der = Pt.infer_derivs' (Pt.norm_proof' env) der,
+            tags = [],
             maxidx = maxidx_tpairs tpairs' (maxidx_of_term prop'),
             shyps = may_insert_env_sorts (Theory.deref thy_ref) env shyps,
             hyps = hyps,
@@ -1032,7 +1052,7 @@
 fun generalize ([], []) _ th = th
   | generalize (tfrees, frees) idx th =
       let
-        val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = th;
+        val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = th;
         val _ = idx <= maxidx andalso raise THM ("generalize: bad index", idx, [th]);
 
         val bad_type = if null tfrees then K false else
@@ -1054,6 +1074,7 @@
         Thm {
           thy_ref = thy_ref,
           der = Pt.infer_derivs' (Pt.generalize (tfrees, frees) idx) der,
+          tags = [],
           maxidx = maxidx',
           shyps = shyps,
           hyps = hyps,
@@ -1126,6 +1147,7 @@
         Thm {thy_ref = thy_ref',
           der = Pt.infer_derivs' (fn d =>
             Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+          tags = [],
           maxidx = maxidx',
           shyps = shyps',
           hyps = hyps,
@@ -1145,6 +1167,7 @@
   else
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' I (false, Pt.AbsP ("H", NONE, Pt.PBound 0)),
+      tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
@@ -1159,6 +1182,7 @@
   in
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.class_triv:" ^ c, t, SOME [])),
+      tags = [],
       maxidx = maxidx,
       shyps = sorts,
       hyps = [],
@@ -1169,7 +1193,7 @@
 (*Internalize sort constraints of type variable*)
 fun unconstrainT
     (Ctyp {thy_ref = thy_ref1, T, ...})
-    (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop}) =
+    (th as Thm {thy_ref = thy_ref2, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   let
     val ((x, i), S) = Term.dest_TVar T handle TYPE _ =>
       raise THM ("unconstrainT: not a type variable", 0, [th]);
@@ -1179,6 +1203,7 @@
   in
     Thm {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
       der = Pt.infer_derivs' I (false, Pt.PAxm ("ProtoPure.unconstrainT", prop, SOME [])),
+      tags = [],
       maxidx = Int.max (maxidx, i),
       shyps = Sorts.remove_sort S shyps,
       hyps = hyps,
@@ -1187,7 +1212,7 @@
   end;
 
 (* Replace all TFrees not fixed or in the hyps by new TVars *)
-fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun varifyT' fixed (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   let
     val tfrees = foldr add_term_tfrees fixed hyps;
     val prop1 = attach_tpairs tpairs prop;
@@ -1196,6 +1221,7 @@
   in
     (al, Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' (Pt.varify_proof prop tfrees) der,
+      tags = [],
       maxidx = Int.max (0, maxidx),
       shyps = shyps,
       hyps = hyps,
@@ -1206,7 +1232,7 @@
 val varifyT = #2 o varifyT' [];
 
 (* Replace all TVars by new TFrees *)
-fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun freezeT (Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   let
     val prop1 = attach_tpairs tpairs prop;
     val prop2 = Type.freeze prop1;
@@ -1214,6 +1240,7 @@
   in
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' (Pt.freezeT prop1) der,
+      tags = [],
       maxidx = maxidx_of_term prop2,
       shyps = shyps,
       hyps = hyps,
@@ -1246,6 +1273,7 @@
     else
       Thm {thy_ref = merge_thys1 goal orule,
         der = Pt.infer_derivs' (Pt.lift_proof gprop inc prop) der,
+        tags = [],
         maxidx = maxidx + inc,
         shyps = Sorts.union shyps sorts,  (*sic!*)
         hyps = hyps,
@@ -1253,13 +1281,14 @@
         prop = Logic.list_implies (map lift_all As, lift_all B)}
   end;
 
-fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun incr_indexes i (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...}) =
   if i < 0 then raise THM ("negative increment", 0, [thm])
   else if i = 0 then thm
   else
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs'
         (Pt.map_proof_terms (Logic.incr_indexes ([], i)) (Logic.incr_tvar i)) der,
+      tags = [],
       maxidx = maxidx + i,
       shyps = shyps,
       hyps = hyps,
@@ -1277,6 +1306,7 @@
         der = Pt.infer_derivs'
           ((if Envir.is_empty env then I else (Pt.norm_proof' env)) o
             Pt.assumption_proof Bs Bi n) der,
+        tags = [],
         maxidx = maxidx,
         shyps = may_insert_env_sorts thy env shyps,
         hyps = hyps,
@@ -1307,6 +1337,7 @@
     | n =>
         Thm {thy_ref = thy_ref,
           der = Pt.infer_derivs' (Pt.assumption_proof Bs Bi (n + 1)) der,
+          tags = [],
           maxidx = maxidx,
           shyps = shyps,
           hyps = hyps,
@@ -1335,6 +1366,7 @@
   in
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' (Pt.rotate_proof Bs Bi m) der,
+      tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,
@@ -1348,7 +1380,7 @@
   number of premises.  Useful with etac and underlies defer_tac*)
 fun permute_prems j k rl =
   let
-    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop} = rl;
+    val Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop, ...} = rl;
     val prems = Logic.strip_imp_prems prop
     and concl = Logic.strip_imp_concl prop;
     val moved_prems = List.drop (prems, j)
@@ -1365,6 +1397,7 @@
   in
     Thm {thy_ref = thy_ref,
       der = Pt.infer_derivs' (Pt.permute_prems_prf prems j m) der,
+      tags = [],
       maxidx = maxidx,
       shyps = shyps,
       hyps = hyps,
@@ -1381,7 +1414,7 @@
   preceding parameters may be renamed to make all params distinct.*)
 fun rename_params_rule (cs, i) state =
   let
-    val Thm {thy_ref, der, maxidx, shyps, hyps, ...} = state;
+    val Thm {thy_ref, der, tags, maxidx, shyps, hyps, ...} = state;
     val (tpairs, Bs, Bi, C) = dest_state (state, i);
     val iparams = map #1 (Logic.strip_params Bi);
     val short = length iparams - length cs;
@@ -1399,6 +1432,7 @@
       | [] =>
         Thm {thy_ref = thy_ref,
           der = der,
+          tags = tags,
           maxidx = maxidx,
           shyps = shyps,
           hyps = hyps,
@@ -1409,12 +1443,13 @@
 
 (*** Preservation of bound variable names ***)
 
-fun rename_boundvars pat obj (thm as Thm {thy_ref, der, maxidx, shyps, hyps, tpairs, prop}) =
+fun rename_boundvars pat obj (thm as Thm {thy_ref, der, tags, maxidx, shyps, hyps, tpairs, prop}) =
   (case Term.rename_abs pat obj prop of
     NONE => thm
   | SOME prop' => Thm
       {thy_ref = thy_ref,
        der = der,
+       tags = tags,
        maxidx = maxidx,
        hyps = hyps,
        shyps = shyps,
@@ -1535,6 +1570,7 @@
                      else
                        curry op oo (Pt.norm_proof' env))
                     (Pt.bicompose_proof flatten Bs oldAs As A n)) rder' sder,
+                 tags = [],
                  maxidx = maxidx,
                  shyps = may_insert_env_sorts thy env (Sorts.union rshyps sshyps),
                  hyps = union_hyps rhyps shyps,
@@ -1632,6 +1668,7 @@
         else
           Thm {thy_ref = Theory.self_ref thy',
             der = (true, Pt.oracle_proof name prop),
+            tags = [],
             maxidx = maxidx,
             shyps = may_insert_term_sorts thy' prop [],
             hyps = [],