TFL/usyntax.sig
changeset 3353 9112a2efb9a3
parent 3330 ab7161e593c8
child 3391 5e45dd3b64e9
--- a/TFL/usyntax.sig	Tue May 27 13:03:41 1997 +0200
+++ b/TFL/usyntax.sig	Tue May 27 13:22:30 1997 +0200
@@ -10,8 +10,6 @@
 sig
   structure Utils : Utils_sig
 
-  type 'a binding
-
   datatype lambda = VAR   of {Name : string, Ty : typ}
                   | CONST of {Name : string, Ty : typ}
                   | COMB  of {Rator: term, Rand : term}
@@ -28,7 +26,6 @@
   val -->        : typ * typ -> typ
   val strip_type : typ -> typ list * typ
   val strip_prod_type : typ -> typ list
-  val match_type: typ -> typ -> typ binding list
 
   (* Terms *)
   val free_vars  : term -> term list
@@ -42,8 +39,7 @@
   
   (* Prelogic *)
   val aconv     : term -> term -> bool
-  val subst     : term binding list -> term -> term
-  val inst      : typ binding list -> term -> term
+  val inst      : (typ*typ) list -> term -> term
   val beta_conv : term -> term
 
   (* Construction routines *)