Improved comments.

--- a/src/Provers/eqsubst.ML	Wed Apr 18 11:47:08 2007 +0200
+++ b/src/Provers/eqsubst.ML	Wed Apr 18 16:23:31 2007 +0200
@@ -65,11 +65,15 @@
        int -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
     val eqsubst_tac :
        Proof.context ->
-       int list -> Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
+       int list -> (* list of occurences to rewrite, use [0] for any *)
+       Thm.thm list -> int -> Thm.thm -> Thm.thm Seq.seq
     val eqsubst_tac' :
-       Proof.context ->
-       (searchinfo -> Term.term -> match Seq.seq) 
-       -> Thm.thm -> int -> Thm.thm -> Thm.thm Seq.seq
+       Proof.context -> (* proof context *)
+       (searchinfo -> Term.term -> match Seq.seq) (* search function *)
+       -> Thm.thm (* equation theorem to rewrite with *)
+       -> int (* subgoal number in goal theorem *)
+       -> Thm.thm (* goal theorem *)
+       -> Thm.thm Seq.seq (* rewritten goal theorem *)
 
 
     val fakefree_badbounds :
@@ -383,6 +387,11 @@
       SkipMore _ => Seq.empty
     | SkipSeq ss => Seq.flat ss;
 
+(* The occL is a list of integers indicating which occurence
+w.r.t. the search order, to rewrite. Backtracking will also find later
+occurences, but all earlier ones are skipped. Thus you can use [0] to
+just find all rewrites. *)
+
 fun eqsubst_tac ctxt occL thms i th =
     let val nprems = Thm.nprems_of th in
       if nprems < i then Seq.empty else