TFL/rules.sig
changeset 3353 9112a2efb9a3
parent 3302 404fe31fd8d2
child 3379 7091ffa99c93
--- a/TFL/rules.sig	Tue May 27 13:03:41 1997 +0200
+++ b/TFL/rules.sig	Tue May 27 13:22:30 1997 +0200
@@ -9,8 +9,6 @@
 signature Rules_sig =
 sig
 (*  structure USyntax : USyntax_sig *)
-  type 'a binding
-
   val dest_thm : thm -> term list * term
 
   (* Inference rules *)
@@ -23,7 +21,7 @@
   val CONJUNCTS :thm -> thm list
   val DISCH     :cterm -> thm -> thm
   val UNDISCH   :thm  -> thm
-  val INST_TYPE :typ binding list -> thm -> thm
+  val INST_TYPE :(typ*typ)list -> thm -> thm
   val SPEC      :cterm -> thm -> thm
   val ISPEC     :cterm -> thm -> thm
   val ISPECL    :cterm list -> thm -> thm
@@ -42,7 +40,7 @@
   val CHOOSE : cterm * thm -> thm -> thm
   val EXISTS : cterm * cterm -> thm -> thm
   val EXISTL : cterm list -> thm -> thm
-  val IT_EXISTS : cterm binding list -> thm -> thm
+  val IT_EXISTS : (cterm*cterm) list -> thm -> thm
 
   val EVEN_ORS : thm list -> thm list
   val DISJ_CASESL : thm -> thm list -> thm