diff -r 41ce0b56d858 -r 7f11d833d65b src/Tools/Metis/src/Subst.sig
--- a/src/Tools/Metis/src/Subst.sig	Mon Sep 13 16:44:20 2010 +0200
+++ b/src/Tools/Metis/src/Subst.sig	Mon Sep 13 21:24:10 2010 +0200
@@ -1,6 +1,6 @@
 (* ========================================================================= *)
 (* FIRST ORDER LOGIC SUBSTITUTIONS                                           *)
-(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *)
+(* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License       *)
 (* ========================================================================= *)
 
 signature Subst =
@@ -28,8 +28,6 @@
 
 val singleton : Term.var * Term.term -> subst
 
-val union : subst -> subst -> subst
-
 val toList : subst -> (Term.var * Term.term) list
 
 val fromList : (Term.var * Term.term) list -> subst
@@ -38,7 +36,7 @@
 
 val foldr : (Term.var * Term.term * 'a -> 'a) -> 'a -> subst -> 'a
 
-val pp : subst Parser.pp
+val pp : subst Print.pp
 
 val toString : subst -> string
 
@@ -71,7 +69,13 @@
 val compose : subst -> subst -> subst
 
 (* ------------------------------------------------------------------------- *)
-(* Substitutions can be inverted iff they are renaming substitutions.        *) 
+(* Creating the union of two compatible substitutions.                       *)
+(* ------------------------------------------------------------------------- *)
+
+val union : subst -> subst -> subst  (* raises Error *)
+
+(* ------------------------------------------------------------------------- *)
+(* Substitutions can be inverted iff they are renaming substitutions.        *)
 (* ------------------------------------------------------------------------- *)
 
 val invert : subst -> subst  (* raises Error *)
@@ -85,6 +89,22 @@
 val freshVars : NameSet.set -> subst
 
 (* ------------------------------------------------------------------------- *)
+(* Free variables.                                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val redexes : subst -> NameSet.set
+
+val residueFreeVars : subst -> NameSet.set
+
+val freeVars : subst -> NameSet.set
+
+(* ------------------------------------------------------------------------- *)
+(* Functions.                                                                *)
+(* ------------------------------------------------------------------------- *)
+
+val functions : subst -> NameAritySet.set
+
+(* ------------------------------------------------------------------------- *)
 (* Matching for first order logic terms.                                     *)
 (* ------------------------------------------------------------------------- *)