# HG changeset patch
# User wenzelm
# Date 916151974 -3600
# Node ID 04515352f19ecf92f5d2e9e7bfedb72fb5dfed18
# Parent  3451f9e885285e17d23c9321dac20e26b9588d2a
fixed deriv;

diff -r 3451f9e88528 -r 04515352f19e doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Tue Jan 12 15:25:53 1999 +0100
+++ b/doc-src/Ref/thm.tex	Tue Jan 12 15:39:34 1999 +0100
@@ -773,7 +773,7 @@
 record: 
 \begin{ttbox} 
 #der (rep_thm conjI);
-{\out Join (Theorem "HOL.conjI", [Join (MinProof,[])]) : deriv}
+{\out Join (Theorem ("HOL.conjI", []), [Join (MinProof,[])]) : deriv}
 \end{ttbox}
 This proof object identifies a labelled theorem, {\tt conjI} of theory
 \texttt{HOL}, whose underlying proof has not been recorded; all we