diff -r b38c67991122 -r 2d3d020eef11 doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Wed Jan 18 11:36:04 1995 +0100
+++ b/doc-src/Ref/thm.tex	Thu Jan 19 16:05:21 1995 +0100
@@ -166,7 +166,7 @@
 \end{ttdescription}
 
 
-\subsection{Miscellaneous forward rules}
+\subsection{Miscellaneous forward rules}\label{MiscellaneousForwardRules}
 \index{theorems!standardizing}
 \begin{ttbox} 
 standard         :           thm -> thm
@@ -209,6 +209,7 @@
 nprems_of     : thm -> int
 tpairs_of     : thm -> (term*term)list
 stamps_of_thy : thm -> string ref list
+theory_of_thm : thm -> theory
 dest_state    : thm*int -> (term*term)list*term list*term*term
 rep_thm       : thm -> \{prop:term, hyps:term list, 
                         maxidx:int, sign:Sign.sg\}
@@ -230,6 +231,9 @@
 \item[\ttindexbold{stamps_of_thm} $thm$] 
 returns the \rmindex{stamps} of the signature associated with~$thm$.
 
+\item[\ttindexbold{theory_of_thm} $thm$]
+returns the theory associated with $thm$.
+
 \item[\ttindexbold{dest_state} $(thm,i)$] 
 decomposes $thm$ as a tuple containing a list of flex-flex constraints, a
 list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem