# HG changeset patch # User haftmann # Date 1160571101 -7200 # Node ID 5bfa2e4ed789d5482de1fcec4be812c2d8828c8c # Parent 2a29a21825d16f26c8eb59ef4a00b36a54326f40 adapted to signature change diff -r 2a29a21825d1 -r 5bfa2e4ed789 doc-src/Ref/substitution.tex --- a/doc-src/Ref/substitution.tex Wed Oct 11 14:51:25 2006 +0200 +++ b/doc-src/Ref/substitution.tex Wed Oct 11 14:51:41 2006 +0200 @@ -126,7 +126,7 @@ sig structure Simplifier : SIMPLIFIER val dest_Trueprop : term -> term - val dest_eq : term -> term*term*typ + val dest_eq : term -> (term*term)*typ val dest_imp : term -> term*term val eq_reflection : thm (* a=b ==> a==b *) val rev_eq_reflection: thm (* a==b ==> a=b *) @@ -146,7 +146,7 @@ corresponding object-level one. Typically, it should return $P$ when applied to the term $\texttt{Trueprop}\,P$ (see example below). -\item[\ttindexbold{dest_eq}] should return the triple~$(t,u,T)$, where $T$ is +\item[\ttindexbold{dest_eq}] should return the triple~$((t,u),T)$, where $T$ is the type of~$t$ and~$u$, when applied to the \ML{} term that represents~$t=u$. For other terms, it should raise an exception. @@ -188,7 +188,7 @@ fun dest_Trueprop (Const ("Trueprop", _) $ P) = P | dest_Trueprop t = raise TERM ("dest_Trueprop", [t]); -fun dest_eq (Const("op =",T) $ t $ u) = (t, u, domain_type T) +fun dest_eq (Const("op =",T) $ t $ u) = ((t, u), domain_type T) fun dest_imp (Const("op -->",_) $ A $ B) = (A, B) | dest_imp t = raise TERM ("dest_imp", [t]);