Deleted unused functions

--- a/TFL/dcterm.sml	Mon May 26 12:26:35 1997 +0200
+++ b/TFL/dcterm.sml	Mon May 26 12:27:58 1997 +0200
@@ -28,11 +28,8 @@
     val dest_pair : cterm -> cterm * cterm
     val dest_select : cterm -> cterm * cterm
     val dest_var : cterm -> {Name:string, Ty:typ}
-    val is_abs : cterm -> bool
-    val is_comb : cterm -> bool
     val is_conj : cterm -> bool
     val is_cons : cterm -> bool
-    val is_const : cterm -> bool
     val is_disj : cterm -> bool
     val is_eq : cterm -> bool
     val is_exists : cterm -> bool
@@ -42,7 +39,6 @@
     val is_neg : cterm -> bool
     val is_pair : cterm -> bool
     val is_select : cterm -> bool
-    val is_var : cterm -> bool
     val list_mk_abs : cterm list -> cterm -> cterm
     val list_mk_exists : cterm list * cterm -> cterm
     val list_mk_forall : cterm list * cterm -> cterm
@@ -66,7 +62,6 @@
  * General support routines
  *---------------------------------------------------------------------------*)
 val can = Utils.can;
-val quote = Utils.quote;
 fun swap (x,y) = (y,x);
 
 fun itlist f L base_value =
@@ -171,10 +166,6 @@
 
 (* Query routines *)
 
-val is_var    = can dest_var
-val is_const  = can dest_const
-val is_comb   = can dest_comb
-val is_abs    = can dest_abs
 val is_eq     = can dest_eq
 val is_imp    = can dest_imp
 val is_select = can dest_select

--- 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;

--- a/TFL/usyntax.sml	Mon May 26 12:26:35 1997 +0200
+++ b/TFL/usyntax.sml	Mon May 26 12:27:58 1997 +0200
@@ -212,10 +212,6 @@
                                end
   | dest_term(Bound _)       = raise ERR{func = "dest_term",mesg = "Bound"};
 
-fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty}
-  | dest_var(Free(s,ty))    = {Name = s, Ty = ty}
-  | dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"};
-
 fun dest_const(Const(s,ty)) = {Name = s, Ty = ty}
   | dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};
 
@@ -290,8 +286,6 @@
   
 
 (* Query routines *)
-val is_var    = can dest_var
-val is_const  = can dest_const
 val is_comb   = can dest_comb
 val is_abs    = can dest_abs
 val is_eq     = can dest_eq
@@ -433,8 +427,6 @@
    end;
 
 
-val Term_to_string = string_of_cterm;
-
 fun dest_relation tm =
    if (type_of tm = HOLogic.boolT)
    then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm

--- a/TFL/utils.sig	Mon May 26 12:26:35 1997 +0200
+++ b/TFL/utils.sig	Mon May 26 12:27:58 1997 +0200
@@ -31,8 +31,6 @@
   val zip3 : 'a list -> 'b list -> 'c list -> ('a*'b*'c) list
   val take  : ('a -> 'b) -> int * 'a list -> 'b list
   val sort  : ('a -> 'a -> bool) -> 'a list -> 'a list
-  val concat : string -> string -> string
-  val quote : string -> string
 
 end;
 

--- a/TFL/utils.sml	Mon May 26 12:26:35 1997 +0200
+++ b/TFL/utils.sml	Mon May 26 12:27:58 1997 +0200
@@ -30,9 +30,6 @@
 
 fun C f x y = f y x
 
-val concat = curry (op ^)
-fun quote s = "\""^s^"\"";
-
 fun itlist f L base_value =
    let fun it [] = base_value
          | it (a::rst) = f a (it rst)