lucas - bugfix to subst in assumptions: fixed index error for conditional rules.

--- a/src/Provers/eqsubst.ML	Wed May 18 23:49:52 2005 +0200
+++ b/src/Provers/eqsubst.ML	Thu May 19 01:22:53 2005 +0200
@@ -232,9 +232,6 @@
       |> IsaND.unfix_frees cfvs
       |> RWInst.beta_eta_contract
       |> (fn r => Tactic.rtac r i th);
-(*
- |> (fn r => Thm.bicompose false (false, r, Thm.nprems_of r) i th)
-*)
 
 (* substitute within the conclusion of goal i of gth, using a meta
 equation rule. Note that we assume rule has var indicies zero'd *)
@@ -330,7 +327,7 @@
           HEADGOAL ( Method.insert_tac facts THEN' eqsubst_tac occL inthms ));
 
 (* apply a substitution inside assumption j, keeps asm in the same place *)
-fun apply_subst_in_asm i th rule ((cfvs, j, nprems, pth),m) = 
+fun apply_subst_in_asm i th rule ((cfvs, j, ngoalprems, pth),m) = 
     let 
       val th2 = Thm.rotate_rule (j - 1) i th; (* put premice first *)
       val preelimrule = 
@@ -339,18 +336,21 @@
             |> Thm.permute_prems 0 ~1 (* put old asm first *)
             |> IsaND.unfix_frees cfvs (* unfix any global params *)
             |> RWInst.beta_eta_contract; (* normal form *)
-      val elimrule = 
+  (*    val elimrule = 
           preelimrule
             |> Tactic.make_elim (* make into elim rule *)
             |> Thm.lift_rule (th2, i); (* lift into context *)
+   *)
     in
       (* ~j because new asm starts at back, thus we subtract 1 *)
-      Seq.map (Thm.rotate_rule (~j) (nprems + i))
-              (Thm.bicompose 
+      Seq.map (Thm.rotate_rule (~j) ((Thm.nprems_of rule) + i))
+      (Tactic.dtac preelimrule i th2)
+
+      (* (Thm.bicompose 
                  false (* use unification *)
                  (true, (* elim resolution *)
-                  elimrule, 2 + nprems) 
-                 i th2)
+                  elimrule, (2 + (Thm.nprems_of rule)) - ngoalprems)
+                 i th2) *)
     end;