doc-src/Ref/substitution.tex
changeset 20975 5bfa2e4ed789
parent 9695 ec7d7f877712
child 30184 37969710e61f
     1.1 --- a/doc-src/Ref/substitution.tex	Wed Oct 11 14:51:25 2006 +0200
     1.2 +++ b/doc-src/Ref/substitution.tex	Wed Oct 11 14:51:41 2006 +0200
     1.3 @@ -126,7 +126,7 @@
     1.4    sig
     1.5    structure Simplifier : SIMPLIFIER
     1.6    val dest_Trueprop    : term -> term
     1.7 -  val dest_eq          : term -> term*term*typ
     1.8 +  val dest_eq          : term -> (term*term)*typ
     1.9    val dest_imp         : term -> term*term
    1.10    val eq_reflection    : thm         (* a=b ==> a==b *)
    1.11    val rev_eq_reflection: thm         (* a==b ==> a=b *)
    1.12 @@ -146,7 +146,7 @@
    1.13    corresponding object-level one.  Typically, it should return $P$ when
    1.14    applied to the term $\texttt{Trueprop}\,P$ (see example below).
    1.15    
    1.16 -\item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is
    1.17 +\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is
    1.18    the type of~$t$ and~$u$, when applied to the \ML{} term that
    1.19    represents~$t=u$.  For other terms, it should raise an exception.
    1.20    
    1.21 @@ -188,7 +188,7 @@
    1.22  fun dest_Trueprop (Const ("Trueprop", _) $ P) = P
    1.23    | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]);
    1.24  
    1.25 -fun dest_eq (Const("op =",T)  $ t $ u) = (t, u, domain_type T)
    1.26 +fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T)
    1.27  
    1.28  fun dest_imp (Const("op -->",_) $ A $ B) = (A, B)
    1.29    | dest_imp  t = raise TERM ("dest_imp", [t]);