--- a/src/Provers/eqsubst.ML Wed Feb 23 15:19:00 2005 +0100
+++ b/src/Provers/eqsubst.ML Sun Feb 27 00:00:40 2005 +0100
@@ -27,6 +27,12 @@
signature EQSUBST_TAC =
sig
+ type match =
+ ((Term.indexname * Term.typ) list (* type instantiations *)
+ * (Term.indexname * Term.term) list) (* term instantiations *)
+ * (string * Term.typ) list (* type abs env *)
+ * Term.term (* outer term *)
+
val prep_subst_in_asm :
(Sign.sg (* sign for matching *)
-> int (* maxidx *)
@@ -61,10 +67,7 @@
* int (* num of premises of asm *)
* Thm.thm) (* premthm *)
-> Thm.thm (* rule *)
- -> (((Term.indexname * Term.typ) list (* type instantiations *)
- * (Term.indexname * Term.term) list) (* term instantiations *)
- * (string * Term.typ) list (* type abs env *)
- * Term.term) (* outer term *)
+ -> match
-> Thm.thm Seq.seq
val prep_concl_subst :
@@ -80,10 +83,7 @@
* Thm.thm (* trivial thm of goal concl *)
(* possible matches/unifiers *)
-> Thm.thm (* rule *)
- -> (((Term.indexname * Term.typ) list (* type instantiations *)
- * (Term.indexname * Term.term) list ) (* term instantiations *)
- * (string * Term.typ) list (* Type abs env *)
- * Term.term) (* outer term *)
+ -> match
-> Thm.thm Seq.seq (* substituted goal *)
val eqsubst_asm_meth : Thm.thm list -> Proof.method
@@ -102,6 +102,14 @@
: EQSUBST_TAC
= struct
+ (* a type abriviation for match infomration *)
+ type match =
+ ((Term.indexname * Term.typ) list (* type instantiations *)
+ * (Term.indexname * Term.term) list) (* term instantiations *)
+ * (string * Term.typ) list (* type abs env *)
+ * Term.term (* outer term *)
+
+
(* FOR DEBUGGING...
type trace_subst_errT = int (* subgoal *)
* Thm.thm (* thm with all goals *)