Deleted an obsolete description of rewrite_cterm. The current version uses
meta-simpsets, which are undocumented

--- a/doc-src/Ref/thm.tex	Wed Sep 03 16:25:30 1997 +0200
+++ b/doc-src/Ref/thm.tex	Thu Sep 04 17:43:16 1997 +0200
@@ -663,7 +663,6 @@
 trivial            : cterm -> thm
 lift_rule          : (thm * int) -> thm -> thm
 rename_params_rule : string list * int -> thm -> thm
-rewrite_cterm      : thm list -> cterm -> thm
 flexflex_rule      : thm -> thm Sequence.seq
 \end{ttbox}
 \begin{ttdescription}
@@ -683,12 +682,6 @@
 ensure that all the parameters are distinct.
 \index{parameters!renaming}
 
-\item[\ttindexbold{rewrite_cterm} $defs$ $ct$]
-transforms $ct$ to $ct'$ by repeatedly applying $defs$ as rewrite rules; it
-returns the conclusion~$ct\equiv ct'$.  This underlies the meta-rewriting
-tactics and rules.
-\index{meta-rewriting!in terms}
-
 \item[\ttindexbold{flexflex_rule} $thm$]  \index{flex-flex constraints}
 removes all flex-flex pairs from $thm$ using the trivial unifier.
 \end{ttdescription}