diff -r 7b43a1e74930 -r ab7161e593c8 TFL/usyntax.sig
--- a/TFL/usyntax.sig	Mon May 26 12:26:35 1997 +0200
+++ b/TFL/usyntax.sig	Mon May 26 12:27:58 1997 +0200
@@ -61,7 +61,6 @@
   val mk_pabs   :{varstruct : term, body : term} -> term
 
   (* Destruction routines *)
-  val dest_var  : term -> {Name : string, Ty : typ}
   val dest_const: term -> {Name : string, Ty : typ}
   val dest_comb : term -> {Rator : term, Rand : term}
   val dest_abs  : term -> {Bvar : term, Body : term}
@@ -85,10 +84,6 @@
   
 
   (* Query routines *)
-  val is_var  : term -> bool
-  val is_const: term -> bool
-  val is_comb : term -> bool
-  val is_abs  : term -> bool
   val is_eq     : term -> bool
   val is_imp    : term -> bool
   val is_forall : term -> bool 
@@ -125,7 +120,4 @@
   val dest_relation : term -> term * term * term
   val is_WFR : term -> bool
   val ARB : typ -> term
-
-  (* Prettyprinting *)
-  val Term_to_string : cterm -> string
 end;