# HG changeset patch
# User paulson
# Date 881585839 -3600
# Node ID 25704541008b6f6e579dc4f8908fdb506e6e6d93
# Parent  c1536da54f5233df371bce6c969ae88c85c12d87
Tidying to fix overfull lines, etc

diff -r c1536da54f52 -r 25704541008b doc-src/Ref/ref.ind
--- a/doc-src/Ref/ref.ind	Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/ref.ind	Mon Dec 08 13:57:19 1997 +0100
@@ -347,7 +347,7 @@
   \item {\tt inst_step_tac}, \bold{130}
   \item {\tt instance} section, 53
   \item {\tt instantiate}, \bold{46}
-  \item {\tt instantiate'}, \bold{39}
+  \item {\tt instantiate'}, \bold{39}, 46
   \item instantiation, 18, 39, 46
   \item {\tt INTLEAVE}, \bold{29}, 31
   \item {\tt INTLEAVE'}, 36
@@ -381,7 +381,7 @@
 
   \item macros, 86--92
   \item {\tt make_elim}, \bold{40}, 125
-  \item {\tt Match} exception, 93, 99
+  \item {\tt Match} exception, 94, 99
   \item {\tt match_tac}, \bold{18}, 124
   \item {\tt max_pri}, 66, \bold{72}
   \item {\tt merge_ss}, 107
@@ -601,7 +601,7 @@
   \item {\tt show_brackets}, \bold{4}
   \item {\tt show_consts}, \bold{4}
   \item {\tt show_hyps}, \bold{4}
-  \item {\tt show_sorts}, \bold{4}, 85
+  \item {\tt show_sorts}, \bold{4}, 85, 93
   \item {\tt show_types}, \bold{4}, 85, 88, 95
   \item {\tt Sign.sg} ML type, 51
   \item {\tt Sign.stamp_names_of}, \bold{59}
@@ -799,6 +799,7 @@
   \item type unknowns, \bold{62}, 68
     \subitem freezing/thawing of, 46
   \item type variables, \bold{62}
+  \item {\tt typed_print_translation}, 93
   \item types, \bold{62}
     \subitem certified, \bold{62}
     \subitem printing of, 4, 15, 62
diff -r c1536da54f52 -r 25704541008b doc-src/Ref/ref.tex
--- a/doc-src/Ref/ref.tex	Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/ref.tex	Mon Dec 08 13:57:19 1997 +0100
@@ -1,12 +1,5 @@
 \documentclass[12pt]{report}
-\usepackage{a4}
-
-\makeatletter
-\input{../proof.sty}
-\input{../rail.sty}
-\input{../iman.sty}
-\input{../extra.sty}
-\makeatother
+\usepackage{a4,../iman,../extra,../proof,../rail}
 
 %% $Id$
 %%\includeonly{}
diff -r c1536da54f52 -r 25704541008b doc-src/Ref/thm.tex
--- a/doc-src/Ref/thm.tex	Mon Dec 08 13:56:49 1997 +0100
+++ b/doc-src/Ref/thm.tex	Mon Dec 08 13:57:19 1997 +0100
@@ -132,13 +132,13 @@
 \end{ttdescription}
 
 
-\subsection{Instantiating a theorem} \label{sec:instantiate}
+\subsection{Instantiating unknowns in a theorem} \label{sec:instantiate}
 \index{instantiation}
 \begin{ttbox}
-read_instantiate    :                (string * string) list -> thm -> thm
-read_instantiate_sg :     Sign.sg -> (string * string) list -> thm -> thm
-cterm_instantiate   :                  (cterm * cterm) list -> thm -> thm
-instantiate'        : ctyp option list -> cterm option list -> thm -> thm
+read_instantiate    :                (string*string) list -> thm -> thm
+read_instantiate_sg :     Sign.sg -> (string*string) list -> thm -> thm
+cterm_instantiate   :                  (cterm*cterm) list -> thm -> thm
+instantiate'      : ctyp option list -> cterm option list -> thm -> thm
 \end{ttbox}
 These meta-rules instantiate type and term unknowns in a theorem.  They are
 occasionally useful.  They can prevent difficulties with higher-order
@@ -223,7 +223,7 @@
 prems_of      : thm -> term list
 cprems_of     : thm -> cterm list
 nprems_of     : thm -> int
-tpairs_of     : thm -> (term * term) list
+tpairs_of     : thm -> (term*term) list
 sign_of_thm   : thm -> Sign.sg
 theory_of_thm : thm -> theory
 dest_state    : thm * int -> (term * term) list * term list * term * term