# HG changeset patch
# User paulson
# Date 873387796 -7200
# Node ID 48b8efdd1b80e79009a55c93559d7552e5f2aed5
# Parent  2df8a2bc3ee26da5f7852eb88e31f4c5c43584ef
Deleted an obsolete description of rewrite_cterm.  The current version uses
meta-simpsets, which are undocumented

diff -r 2df8a2bc3ee2 -r 48b8efdd1b80 doc-src/Ref/thm.tex
--- 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}