diff -r 8fb4150e2ad3 -r 79ac9b475621 src/Provers/hypsubst.ML --- a/src/Provers/hypsubst.ML Fri Jul 18 14:06:54 1997 +0200 +++ b/src/Provers/hypsubst.ML Tue Jul 22 11:12:55 1997 +0200 @@ -116,12 +116,11 @@ since e.g. z=f(x); x=z changes to z=f(x); x=f(x) and the second equality must NOT be deleted. Tactic must rotate or delete m assumptions. *) -fun thin_leading_eqs_tac bnd m i = STATE(fn state => +fun thin_leading_eqs_tac bnd m = SUBGOAL (fn (Bi,i) => let fun count [] = 0 | count (A::Bs) = ((inspect_pair bnd true (dest_eq A); 1 + count Bs) handle Match => 0) - val (_,_,Bi,_) = dest_state(state,i) val j = Int.min(m, count (Logic.strip_assums_hyp Bi)) in REPEAT_DETERM_N j (etac thin_rl i) THEN rotate_tac (m-j) i end); @@ -141,17 +140,16 @@ (*Select a suitable equality assumption and substitute throughout the subgoal Replaces only Bound variables if bnd is true*) - fun gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => - let val (_,_,Bi,_) = dest_state(state,i) - val n = length(Logic.strip_assums_hyp Bi) - 1 + fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => + let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,_) = eq_var bnd true Bi in - EVERY [rotate_tac k i, - asm_full_simp_tac hyp_subst_ss i, - etac thin_rl i, - thin_leading_eqs_tac bnd (n-k) i] + DETERM (EVERY [rotate_tac k i, + asm_full_simp_tac hyp_subst_ss i, + etac thin_rl i, + thin_leading_eqs_tac bnd (n-k) i]) end - handle THM _ => no_tac | EQ_VAR => no_tac)); + handle THM _ => no_tac | EQ_VAR => no_tac); end; @@ -159,18 +157,18 @@ (*Old version of the tactic above -- slower but the only way to handle equalities containing Vars.*) -fun vars_gen_hyp_subst_tac bnd i = DETERM (STATE(fn state => - let val (_,_,Bi,_) = dest_state(state,i) - val n = length(Logic.strip_assums_hyp Bi) - 1 +fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => + let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,symopt) = eq_var bnd false Bi in - EVERY [REPEAT_DETERM_N k (etac rev_mp i), - etac revcut_rl i, - REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (if symopt then ssubst else subst) i, - REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)] + DETERM + (EVERY [REPEAT_DETERM_N k (etac rev_mp i), + etac revcut_rl i, + REPEAT_DETERM_N (n-k) (etac rev_mp i), + etac (if symopt then ssubst else subst) i, + REPEAT_DETERM_N n (rtac imp_intr i THEN rotate_tac ~1 i)]) end - handle THM _ => no_tac | EQ_VAR => no_tac)); + handle THM _ => no_tac | EQ_VAR => no_tac); (*Substitutes for Free or Bound variables*) val hyp_subst_tac =