# HG changeset patch
# User wenzelm
# Date 1028743867 -7200
# Node ID 6f9111705d4fefa022a319d98fba72c3f49a9e5d
# Parent  600f1c93124ffa04a7ae4655d468a1244af56191
tuned;

diff -r 600f1c93124f -r 6f9111705d4f doc-src/Ref/simplifier.tex
--- a/doc-src/Ref/simplifier.tex	Wed Aug 07 20:05:43 2002 +0200
+++ b/doc-src/Ref/simplifier.tex	Wed Aug 07 20:11:07 2002 +0200
@@ -1187,11 +1187,14 @@
 \end{ttbox}
 
 \begin{ttdescription}
-\item[\ttindexbold{simproc}~$sign$~$name$~$lhss$~$proc$] makes $proc$ a
-  simplification procedure for left-hand side patterns $lhss$.  The name just
-  serves as a comment.  The function $proc$ may be invoked by the simplifier
-  for redex positions matched by one of $lhss$ as described below (which are
-  be specified as strings to be read as terms).
+\item[\ttindexbold{Simplifier.simproc}~$sign$~$name$~$lhss$~$proc$] makes
+  $proc$ a simplification procedure for left-hand side patterns $lhss$.  The
+  name just serves as a comment.  The function $proc$ may be invoked by the
+  simplifier for redex positions matched by one of $lhss$ as described below
+  (which are be specified as strings to be read as terms).
+  
+\item[\ttindexbold{Simplifier.simproc_i}] is similar to
+  \verb,Simplifier.simproc,, but takes well-typed terms as pattern argument.
 \end{ttdescription}
 
 Simplification procedures are applied in a two-stage process as
@@ -1230,8 +1233,11 @@
 procedure \texttt{pair_eta_expand_proc} is defined as follows:
 \begin{ttbox}
 val pair_eta_expand_proc =
-  Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
-  (fn _ => fn _ => fn t => case t of Abs _ => Some (mk_meta_eq pair_eta_expand) | _ => None);
+  Simplifier.simproc (Theory.sign_of (the_context ()))
+    "pair_eta_expand" ["f::'a*'b=>'c"]
+    (fn _ => fn _ => fn t =>
+      case t of Abs _ => Some (mk_meta_eq pair_eta_expand)
+      | _ => None);
 \end{ttbox}
 This is an example of using \texttt{pair_eta_expand_proc}:
 \begin{ttbox}