diff -r 4af699cdfe47 -r c07b5b0e8492 src/Pure/Proof/proof_syntax.ML
--- 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)) =